Position is the vector from ?p1 to ?p2.
(Nth-Domain Position 3 3d-Vector-Quantity) (Nth-Domain Position 2 3d-Point) (Nth-Domain Position 1 3d-Point) (= (Position ?P1 ?P2) (- (Position ?P2 ?P1))) (Zero-Element (Position ?P ?P)) (= (Position ?P1 ?P3) (+ (Position ?P1 ?P2) (Position ?P2 ?P3)))
(=> (And (3d-Point ?P1) (3d-Point ?P2)) (<=> (Distance ?P1 ?P2 ?D) (And (Scalar-Quantity ?D) (Quantity.Dimension ?D Length-Dimension) (= ?D (Sqrt (Dot (Position ?P1 ?P2) (Position ?P1 ?P2))))))) (Instance-Of (Position ?P ?P) Zero-Element)