let P, Q, P1 be non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( P in BK_model & Q in BK_model & P1 in absolute implies not between RP3_to_T2 Q, RP3_to_T2 P1, RP3_to_T2 P )
assume A1: ( P in BK_model & Q in BK_model & P1 in absolute ) ; :: thesis: not between RP3_to_T2 Q, RP3_to_T2 P1, RP3_to_T2 P
set P9 = RP3_to_T2 P;
set Q9 = RP3_to_T2 Q;
set P19 = RP3_to_T2 P1;
assume A2: between RP3_to_T2 Q, RP3_to_T2 P1, RP3_to_T2 P ; :: thesis: contradiction
consider u being non zero Element of (TOP-REAL 3) such that
A3: ( P = Dir u & u `3 = 1 & RP3_to_REAL2 P = |[(u `1),(u `2)]| ) by Def05;
consider v being non zero Element of (TOP-REAL 3) such that
A4: ( Q = Dir v & v `3 = 1 & RP3_to_REAL2 Q = |[(v `1),(v `2)]| ) by Def05;
consider w1 being non zero Element of (TOP-REAL 3) such that
A5: ( P1 = Dir w1 & w1 `3 = 1 & RP3_to_REAL2 P1 = |[(w1 `1),(w1 `2)]| ) by Def05;
A6: Tn2TR (RP3_to_T2 P1) in LSeg ((Tn2TR (RP3_to_T2 Q)),(Tn2TR (RP3_to_T2 P))) by A2, GTARSKI2:20;
reconsider u9 = Tn2TR (RP3_to_T2 P1), v9 = Tn2TR (RP3_to_T2 Q), w9 = Tn2TR (RP3_to_T2 P) as Element of (TOP-REAL 2) ;
|[(u9 `1),(u9 `2)]| = |[(w1 `1),(w1 `2)]| by A5, EUCLID:53;
then A7: ( u9 `1 = w1 `1 & u9 `2 = w1 `2 ) by FINSEQ_1:77;
|[(v9 `1),(v9 `2)]| = |[(v `1),(v `2)]| by A4, EUCLID:53;
then A8: ( v9 `1 = v `1 & v9 `2 = v `2 ) by FINSEQ_1:77;
|[(w9 `1),(w9 `2)]| = |[(u `1),(u `2)]| by A3, EUCLID:53;
then A9: ( w9 `1 = u `1 & w9 `2 = u `2 ) by FINSEQ_1:77;
reconsider pu = |[(u9 `1),(u9 `2),1]|, pv = |[(v9 `1),(v9 `2),1]|, pw = |[(w9 `1),(w9 `2),1]| as non zero Element of (TOP-REAL 3) ;
pu in LSeg (pw,pv) by A6, Th45;
then consider r being Real such that
A10: ( 0 <= r & r <= 1 ) and
A11: pu = ((1 - r) * pw) + (r * pv) by RLTOPSP1:76;
now :: thesis: ( Q = Dir pv & P = Dir pw & P1 = Dir pu & pv . 3 = 1 & pw . 3 = 1 & pu = (r * pv) + ((1 - r) * pw) )
thus Q = Dir pv by A4, A8, EUCLID_5:3; :: thesis: ( P = Dir pw & P1 = Dir pu & pv . 3 = 1 & pw . 3 = 1 & pu = (r * pv) + ((1 - r) * pw) )
thus P = Dir pw by A3, A9, EUCLID_5:3; :: thesis: ( P1 = Dir pu & pv . 3 = 1 & pw . 3 = 1 & pu = (r * pv) + ((1 - r) * pw) )
thus P1 = Dir pu by A5, A7, EUCLID_5:3; :: thesis: ( pv . 3 = 1 & pw . 3 = 1 & pu = (r * pv) + ((1 - r) * pw) )
thus pv . 3 = pv `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ; :: thesis: ( pw . 3 = 1 & pu = (r * pv) + ((1 - r) * pw) )
thus pw . 3 = pw `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ; :: thesis: pu = (r * pv) + ((1 - r) * pw)
thus pu = (r * pv) + ((1 - r) * pw) by A11; :: thesis: verum
end;
then P1 is Element of BK_model by A1, A10, Th17;
hence contradiction by A1, BKMODEL2:1, XBOOLE_0:def 4; :: thesis: verum