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

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