let P, Q be POINT of BK-model-Plane; :: according to GTARSKI1:def 5 :: thesis: P,Q equiv Q,P

ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . P = Q & (homography N) . Q = P ) by BKMODEL2:60;

hence P,Q equiv Q,P by Def05; :: thesis: verum

ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . P = Q & (homography N) . Q = P ) by BKMODEL2:60;

hence P,Q equiv Q,P by Def05; :: thesis: verum