let A, Q, B, C be POINT of BK-model-Plane; :: thesis:
consider a being Element of BK_model such that
A1: A = a and
BK_to_T2 A = BK_to_REAL2 a by Def01;
consider q being Element of BK_model such that
A2: Q = q and
BK_to_T2 Q = BK_to_REAL2 q by Def01;
consider b being Element of BK_model such that
A3: B = b and
BK_to_T2 B = BK_to_REAL2 b by Def01;
consider c being Element of BK_model such that
A4: C = c and
BK_to_T2 C = BK_to_REAL2 c by Def01;

suppose b <> c ; :: thesis:

A5: for q1, a1, b1, c1 being POINT of BK-model-Plane st q1 <> a1 holds
ex x being POINT of BK-model-Plane st
( between q1,a1,x & a1,x equiv b1,c1 )

let q1, a1, b1, c1 be POINT of BK-model-Plane; :: thesis:
assume A6: q1 <> a1 ; :: thesis:
reconsider Q1 = q1, A1 = a1, B1 = b1, C1 = c1 as Element of BK_model ;
reconsider pQ1 = Q1, pA1 = A1, pB1 = B1, pC1 = C1 as non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) by Th61;
consider qaR being Element of absolute such that
A7: for p, q, r being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st p = q1 & q = a1 & r = qaR holds
between RP3_to_T2 p, RP3_to_T2 q, RP3_to_T2 r by A6, Th58;
reconsider pqaR = qaR as non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) by Th62;

suppose A8: B1 = C1 ; :: thesis:

reconsider x = a1 as Element of BK_model ;
reconsider x = x as POINT of BK-model-Plane ;
take x ; :: thesis:
Tn2TR (BK_to_T2 a1) in LSeg ((Tn2TR (BK_to_T2 q1)),(Tn2TR (BK_to_T2 x))) by RLTOPSP1:68;
then between BK_to_T2 q1, BK_to_T2 a1, BK_to_T2 x by GTARSKI2:20;
hence between q1,a1,x by Th05; :: thesis:
thus a1,x equiv b1,c1 by A8, Th60; :: thesis:

end;

suppose A9: B1 <> C1 ; :: thesis:

consider bcP being Element of absolute such that
A10: for p, q, r being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st p = b1 & q = c1 & r = bcP holds
between RP3_to_T2 p, RP3_to_T2 q, RP3_to_T2 r by A9, Th58;
reconsider pbcP = bcP as non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) by Th62;
consider N being invertible Matrix of 3,F_Real such that
A11: (homography N) .: absolute = absolute and
A12: (homography N) . B1 = A1 and
A13: (homography N) . bcP = qaR by BKMODEL2:56;
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 A11, BKMODEL2:def 6;
then h in EnsK-isometry by BKMODEL2:def 7;
then reconsider h = homography N as Element of SubGroupK-isometry by BKMODEL2:def 8;
h = homography N ;
then reconsider x = (homography N) . C1 as Element of BK_model by BKMODEL3:36;
reconsider x = x as POINT of BK-model-Plane ;
reconsider px = x as non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) by Th61;
take x ; :: thesis:

thus between q1,a1,x :: thesis:

A14: between RP3_to_T2 pQ1, RP3_to_T2 pA1, RP3_to_T2 pqaR by A7;
( between RP3_to_T2 pB1, RP3_to_T2 pC1, RP3_to_T2 pbcP & h = homography N & pB1 in BK_model & pC1 in BK_model & pbcP in absolute ) by A10;
then A15: between RP3_to_T2 pA1, RP3_to_T2 px, RP3_to_T2 pqaR by A12, A13, Th41;
set tq = RP3_to_T2 pQ1;
set ta = RP3_to_T2 pA1;
set tx = RP3_to_T2 px;
set tr = RP3_to_T2 pqaR;
A16: between RP3_to_T2 pQ1, RP3_to_T2 pA1, RP3_to_T2 px by A15, A14, GTARSKI3:17;

consider pp1 being Element of BK_model such that
A17: q1 = pp1 and
A18: BK_to_T2 q1 = BK_to_REAL2 pp1 by Def01;
consider pp2 being Element of BK_model such that
A19: a1 = pp2 and
A20: BK_to_T2 a1 = BK_to_REAL2 pp2 by Def01;
consider pp3 being Element of BK_model such that
A21: x = pp3 and
A22: BK_to_T2 x = BK_to_REAL2 pp3 by Def01;
thus RP3_to_T2 pQ1 = BK_to_T2 q1 by A17, A18, Th63; :: thesis:
thus RP3_to_T2 pA1 = BK_to_T2 a1 by A19, A20, Th63; :: thesis:
thus RP3_to_T2 px = BK_to_T2 x by Th63, A21, A22; :: thesis:

end;

hence between q1,a1,x by A16, Th05; :: thesis:

end;

ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . a1 = b1 & (homography N) . x = c1 )

A23: h = homography N ;
reconsider M = N ~ as invertible Matrix of 3,F_Real ;
reconsider g = homography M as Element of SubGroupK-isometry by A23, BKMODEL2:47;
take g ; :: thesis:
ex N being invertible Matrix of 3,F_Real st
( g = homography N & (homography N) . a1 = b1 & (homography N) . x = c1 )

take M ; :: thesis:
thus ( g = homography M & (homography M) . a1 = b1 & (homography M) . x = c1 ) by A12, ANPROJ_9:15; :: thesis:

end;

hence ex N being invertible Matrix of 3,F_Real st
( g = homography N & (homography N) . a1 = b1 & (homography N) . x = c1 ) ; :: thesis:

end;

hence a1,x equiv b1,c1 by BKMODEL3:def 8; :: thesis:

end;

hence ( between q1,a1,x & a1,x equiv b1,c1 ) ; :: thesis:

end;

end;

end;

( q = a implies ex x being POINT of BK-model-Plane st
( between Q,A,x & A,x equiv B,C ) )

assume A24: q = a ; :: thesis:
consider Q3 being Element of BK_model such that
A25: a <> Q3 by BKMODEL3:11;
reconsider q3 = Q3 as Element of BK-model-Plane ;
consider x being POINT of BK-model-Plane such that
between q3,A,x and
A26: A,x equiv B,C by A25, A1, A5;
take x ; :: thesis:
between BK_to_T2 A, BK_to_T2 A, BK_to_T2 x by GTARSKI1:17;
hence ( between Q,A,x & A,x equiv B,C ) by A26, A1, A24, A2, Th05; :: thesis:

end;

hence ex x being POINT of BK-model-Plane st
( between Q,A,x & A,x equiv B,C ) by A1, A2, A5; :: thesis:

end;

suppose A27: b = c ; :: thesis:

set X = A;
take A ; :: thesis:
between BK_to_T2 Q, BK_to_T2 A, BK_to_T2 A by GTARSKI1:14;
hence between Q,A,A by Th05; :: thesis:
thus A,A equiv B,C by A27, A3, A4, Th60; :: thesis:

end;

end;