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