let R1, R2 be non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( R1 in absolute & R2 in absolute & R1 <> R2 implies ex P being Element of BK-model-Plane st between RP3_to_T2 R1, BK_to_T2 P, RP3_to_T2 R2 )
assume that
A1: ( R1 in absolute & R2 in absolute ) and
A2: R1 <> R2 ; :: thesis: ex P being Element of BK-model-Plane st between RP3_to_T2 R1, BK_to_T2 P, RP3_to_T2 R2
consider u1 being non zero Element of (TOP-REAL 3) such that
A3: R1 = Dir u1 and
A4: u1 `3 = 1 and
A5: RP3_to_REAL2 R1 = |[(u1 `1),(u1 `2)]| by Def05;
u1 . 3 = 1 by A4, EUCLID_5:def 3;
then |[(u1 . 1),(u1 . 2)]| in circle (0,0,1) by A1, A3, BKMODEL1:84;
then A6: |[(u1 `1),(u1 . 2)]| in circle (0,0,1) by EUCLID_5:def 1;
consider u2 being non zero Element of (TOP-REAL 3) such that
A7: R2 = Dir u2 and
A8: u2 `3 = 1 and
A9: RP3_to_REAL2 R2 = |[(u2 `1),(u2 `2)]| by Def05;
u2 . 3 = 1 by A8, EUCLID_5:def 3;
then |[(u2 . 1),(u2 . 2)]| in circle (0,0,1) by A1, A7, BKMODEL1:84;
then A10: |[(u2 `1),(u2 . 2)]| in circle (0,0,1) by EUCLID_5:def 1;
reconsider P1 = RP3_to_T2 R1, P2 = RP3_to_T2 R2 as Point of TarskiEuclid2Space ;
( Tn2TR P1 in circle (0,0,1) & Tn2TR P2 in circle (0,0,1) & P1 <> P2 ) by A2, Th50, A6, A5, A9, A10, EUCLID_5:def 2;
hence ex P being Element of BK-model-Plane st between RP3_to_T2 R1, BK_to_T2 P, RP3_to_T2 R2 by Th49; :: thesis: verum