let P, Q be Element of BK_model ; :: thesis:
assume A1: P <> Q ; :: thesis:
consider P1, P2, P3, P4 being Element of absolute , P5 being Element of (ProjectiveSpace (TOP-REAL 3)) such that
A2: P1 <> P2 and
A3: P,Q,P1 are_collinear and
A4: P,Q,P2 are_collinear and
A5: P,P5,P3 are_collinear and
A6: Q,P5,P4 are_collinear and
A7: P1,P2,P3 are_mutually_distinct and
A8: P1,P2,P4 are_mutually_distinct and
A9: P5 in (tangent P1) /\ (tangent P2) by A1, Th44;
consider N1 being invertible Matrix of 3,F_Real such that
A10: (homography N1) .: absolute = absolute and
A11: (homography N1) . Dir101 = P1 and
A12: (homography N1) . Dirm101 = P2 and
A13: (homography N1) . Dir011 = P3 and
A14: (homography N1) . Dir010 = P5 by A7, A9, Th37;
P2,P1,P4 are_mutually_distinct by A8;
then consider N2 being invertible Matrix of 3,F_Real such that
A15: (homography N2) .: absolute = absolute and
A16: (homography N2) . Dir101 = P2 and
A17: (homography N2) . Dirm101 = P1 and
A18: (homography N2) . Dir011 = P4 and
A19: (homography N2) . Dir010 = P5 by A9, Th37;
reconsider N = N2 * (N1 ~) as invertible Matrix of 3,F_Real ;
A20: (homography N) . P1 = (homography N2) . ((homography (N1 ~)) . P1) by ANPROJ_9:13
.= P2 by A11, A16, ANPROJ_9:15 ;
A21: (homography N) . P2 = (homography N2) . ((homography (N1 ~)) . P2) by ANPROJ_9:13
.= P1 by A12, A17, ANPROJ_9:15 ;
A22: (homography N) . P3 = (homography N2) . ((homography (N1 ~)) . P3) by ANPROJ_9:13
.= P4 by A13, A18, ANPROJ_9:15 ;
A23: (homography N) . P5 = (homography N2) . ((homography (N1 ~)) . P5) by ANPROJ_9:13
.= P5 by A14, A19, ANPROJ_9:15 ;
homography N1 in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h1 = homography N1 as Element of EnsHomography3 ;
h1 is_K-isometry by A10;
then h1 in EnsK-isometry ;
then reconsider hsg1 = h1 as Element of SubGroupK-isometry by Def05;
homography N2 in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h2 = homography N2 as Element of EnsHomography3 ;
h2 is_K-isometry by A15;
then h2 in EnsK-isometry ;
then reconsider hsg2 = h2 as Element of SubGroupK-isometry by Def05;
homography (N1 ~) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h3 = homography (N1 ~) as Element of EnsHomography3 ;
A24: hsg1 " = h3 by Th36;
set H = EnsK-isometry ;
set G = GroupHomography3 ;
reconsider hg1 = hsg1, hg2 = hsg2, hg3 = hsg1 " as Element of GroupHomography3 by A24, ANPROJ_9:def 4;
reconsider hsg3 = h3 as Element of SubGroupK-isometry by A24;
reconsider h4 = hsg2 * hsg3 as Element of SubGroupK-isometry ;
A25: h4 = hg2 * hg3 by A24, GROUP_2:43
.= h2 (*) h3 by A24, ANPROJ_9:def 3, ANPROJ_9:def 4
.= homography N by ANPROJ_9:18 ;
h4 in the carrier of SubGroupK-isometry ;
then h4 in EnsK-isometry by Def05;
then consider h being Element of EnsHomography3 such that
A26: h4 = h and
A27: h is_K-isometry ;
take N ; :: thesis:
thus (homography N) .: absolute = absolute by A25, A26, A27; :: thesis:
set NP = (homography N) . P;
set NQ = (homography N) . Q;
set NP1 = (homography N) . P1;
set NP2 = (homography N) . P2;
set NP3 = (homography N) . P3;
set NP4 = (homography N) . P4;
set NP5 = (homography N) . P5;
A28: P,P1,P2 are_collinear by A1, A3, A4, ANPROJ_8:57, HESSENBE:2;
( Q,P,P1 are_collinear & Q,P,P2 are_collinear ) by A3, A4, COLLSP:4;
then A29: Q,P1,P2 are_collinear by A1, ANPROJ_8:57, HESSENBE:2;
thus ( (homography N) . P = Q & (homography N) . Q = P ) :: thesis:

proof

A30: (homography N) . P <> (homography N) . Q

proof

assume A31: (homography N) . P = (homography N) . Q ; :: thesis:
Q = (homography (N ~)) . ((homography N) . Q) by ANPROJ_9:15
.= P by A31, ANPROJ_9:15 ;
hence contradiction by A1; :: thesis:

end;

A32: ( (homography N) . P,(homography N) . Q,(homography N) . P1 are_collinear & (homography N) . P,(homography N) . Q,(homography N) . P2 are_collinear & (homography N) . P,(homography N) . P5,(homography N) . P3 are_collinear & (homography N) . Q,(homography N) . P5,(homography N) . P4 are_collinear ) by A3, A4, A5, A6, ANPROJ_8:102;
then A33: (homography N) . P,(homography N) . P1,(homography N) . P2 are_collinear by ANPROJ_8:57, A30, HESSENBE:2;
A34: P1,P2,Q are_collinear by A29, ANPROJ_8:57, HESSENBE:1;
P5,P4,Q are_collinear by A6, ANPROJ_8:57, HESSENBE:1;
then A35: ( Q in Line (P1,P2) & Q in Line (P5,P4) ) by A34, COLLSP:11;
then A36: Q in (Line (P1,P2)) /\ (Line (P5,P4)) by XBOOLE_0:def 4;
P1,P2,(homography N) . P are_collinear by A33, A20, A21, ANPROJ_8:57, HESSENBE:1;
then A37: (homography N) . P in Line (P1,P2) by COLLSP:11;
P5,P4,(homography N) . P are_collinear by A32, A22, A23, ANPROJ_8:57, HESSENBE:1;
then (homography N) . P in Line (P5,P4) by COLLSP:11;
then (homography N) . P in (Line (P5,P4)) /\ (Line (P1,P2)) by A37, XBOOLE_0:def 4;
then A39: {Q,((homography N) . P)} c= (Line (P1,P2)) /\ (Line (P5,P4)) by A36, ZFMISC_1:32;
P4 <> P5

proof

assume P4 = P5 ; :: thesis:
then ( P4 in tangent P1 & P4 in tangent P2 ) by A9, XBOOLE_0:def 4;
then ( P4 in (tangent P1) /\ absolute & P4 in (tangent P2) /\ absolute ) by XBOOLE_0:def 4;
then ( P4 in {P1} & P4 in {P2} ) by Th22;
then ( P4 = P1 & P4 = P2 ) by TARSKI:def 1;
hence contradiction by A2; :: thesis:

end;

then ( Line (P1,P2) is LINE of real_projective_plane & Line (P5,P4) is LINE of real_projective_plane ) by A2, COLLSP:def 7;
then A41: ( Line (P1,P2) = Line (P5,P4) or Line (P1,P2) misses Line (P5,P4) or ex p being Element of real_projective_plane st (Line (P1,P2)) /\ (Line (P5,P4)) = {p} ) by COLLSP:21;
Line (P1,P2) <> Line (P5,P4)

proof

assume Line (P1,P2) = Line (P5,P4) ; :: thesis:
then P4 in Line (P1,P2) by COLLSP:10;
hence contradiction by A8, COLLSP:11, BKMODEL1:92; :: thesis:

end;

then consider p being Element of real_projective_plane such that
A42: (Line (P1,P2)) /\ (Line (P5,P4)) = {p} by A35, A41, XBOOLE_0:def 4;
( Q = p & (homography N) . P = p ) by A42, A39, ZFMISC_1:20;
hence ( (homography N) . P = Q & (homography N) . Q = P ) by A28, A20, A21, A2, COLLSP:8, BKMODEL1:69; :: thesis:

end;

thus 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 A2, A3, A4, A20, A21; :: thesis: