let P, Q be Element of BK_model ; :: thesis:

per cases ;

suppose A1: P = Q ; :: thesis:

reconsider N = 1. (F_Real,3) as invertible Matrix of 3,F_Real ;
homography N in { (homography N) where N is invertible Matrix of 3,F_Real : verum } ;
then reconsider h = homography N as Element of EnsHomography3 by ANPROJ_9:def 1;
h is_K-isometry by Th33;
then h in EnsK-isometry ;
then reconsider h = h as Element of SubGroupK-isometry by Def05;
take h ; :: thesis:
( (homography N) . P = Q & (homography N) . Q = P ) by A1, ANPROJ_9:14;
hence ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . P = Q & (homography N) . Q = P ) ; :: thesis:

end;

suppose P <> Q ; :: thesis:

then consider N being invertible Matrix of 3,F_Real such that
A2: (homography N) .: absolute = absolute and
A3: (homography N) . P = Q and
A4: (homography N) . Q = P and
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 ) by Th45;
homography N in { (homography N) where N is invertible Matrix of 3,F_Real : verum } ;
then reconsider h = homography N as Element of EnsHomography3 by ANPROJ_9:def 1;
h is_K-isometry by A2;
then h in EnsK-isometry ;
then reconsider h = h as Element of SubGroupK-isometry by Def05;
take h ; :: thesis:
thus ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . P = Q & (homography N) . Q = P ) by A3, A4; :: thesis:

end;

end;