theorem Th45: :: BKMODEL2:59

for P, Q being Element of BK_model st P <> Q holds
ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . P = Q & (homography N) . Q = P & ex P1, P2 being Element of absolute st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & (homography N) . P1 = P2 & (homography N) . P2 = P1 ) )