let P, Q, R be Point of BK-model-Plane; :: according to GTARSKI1:def 7 :: thesis: ( not P,Q equiv R,R or P = Q )
assume P,Q equiv R,R ; :: thesis: P = Q
then ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . P = R & (homography N) . Q = R ) by Def05;
hence P = Q by BKMODEL2:62; :: thesis: verum