for P, Q, R, P9, Q9, R9 being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))
for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real st h = homography N & P in BK_model & Q in BK_model & R in absolute & P9 = (homography N) . P & Q9 = (homography N) . Q & R9 = (homography N) . R & between RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R holds
between RP3_to_T2 P9, RP3_to_T2 Q9, RP3_to_T2 R9