let P, Q, R1, R2 be non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( P <> Q & P in BK_model & R1 in absolute & R2 in absolute & between RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R1 & between RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R2 implies R1 = R2 )
assume that
A1: P <> Q and
A2: P in BK_model and
A3: R1 in absolute and
A4: R2 in absolute and
A5: between RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R1 and
A6: between RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R2 ; :: thesis: R1 = R2
assume R1 <> R2 ; :: thesis: contradiction
then consider S being Element of BK-model-Plane such that
A7: between RP3_to_T2 R1, BK_to_T2 S, RP3_to_T2 R2 by A3, A4, Th51;
set p = RP3_to_T2 P;
set q = RP3_to_T2 Q;
set r1 = RP3_to_T2 R1;
set r2 = RP3_to_T2 R2;
set s = BK_to_T2 S;
( ( between RP3_to_T2 P, RP3_to_T2 R1, RP3_to_T2 R2 or between RP3_to_T2 P, RP3_to_T2 R2, RP3_to_T2 R1 ) & between RP3_to_T2 R1, BK_to_T2 S, RP3_to_T2 R2 & between RP3_to_T2 R2, BK_to_T2 S, RP3_to_T2 R1 ) by A7, GTARSKI1:16, A1, A5, A6, Th50, GTARSKI3:56;
per cases then ( between RP3_to_T2 P, RP3_to_T2 R1, BK_to_T2 S or between RP3_to_T2 P, RP3_to_T2 R2, BK_to_T2 S ) by GTARSKI1:19;
suppose A8: between RP3_to_T2 P, RP3_to_T2 R1, BK_to_T2 S ; :: thesis: contradiction
A9: RP3_to_REAL2 R1 in circle (0,0,1) by A3, Th53;
then Tn2TR (RP3_to_T2 R1) in inside_of_circle (0,0,1) by Th52;
then RP3_to_REAL2 R1 in (inside_of_circle (0,0,1)) /\ (circle (0,0,1)) by A9, XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 7, TOPREAL9:54; :: thesis: verum
end;
suppose A10: between RP3_to_T2 P, RP3_to_T2 R2, BK_to_T2 S ; :: thesis: contradiction
A11: RP3_to_REAL2 R2 in circle (0,0,1) by A4, Th53;
then Tn2TR (RP3_to_T2 R2) in inside_of_circle (0,0,1) by Th52;
then RP3_to_REAL2 R2 in (inside_of_circle (0,0,1)) /\ (circle (0,0,1)) by A11, XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 7, TOPREAL9:54; :: thesis: verum
end;
end;