let P1, P2 be Element of absolute ; :: thesis: for Q being Element of BK_model
for u, v, w being non zero Element of (TOP-REAL 3) st Dir u = P1 & Dir v = P2 & Dir w = Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 1 & v . 1 = - (u . 1) & v . 2 = - (u . 2) & P1,Q,P2 are_collinear holds
ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) )
let Q be Element of BK_model ; :: thesis: for u, v, w being non zero Element of (TOP-REAL 3) st Dir u = P1 & Dir v = P2 & Dir w = Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 1 & v . 1 = - (u . 1) & v . 2 = - (u . 2) & P1,Q,P2 are_collinear holds
ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) )
let u, v, w be non zero Element of (TOP-REAL 3); :: thesis: ( Dir u = P1 & Dir v = P2 & Dir w = Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 1 & v . 1 = - (u . 1) & v . 2 = - (u . 2) & P1,Q,P2 are_collinear implies ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) ) )
assume that
A1: ( Dir u = P1 & Dir v = P2 & Dir w = Q ) and
A2: ( u . 3 = 1 & v . 3 = 1 & w . 3 = 1 ) and
A3: ( v . 1 = - (u . 1) & v . 2 = - (u . 2) ) and
A4: P1,Q,P2 are_collinear ; :: thesis: ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) )
( u . 1 = u `1 & u . 2 = u `2 ) by EUCLID_5:def 1, EUCLID_5:def 2;
then A6: ( u `3 = 1 & v `3 = 1 & w `3 = 1 & v `1 = - (u `1) & v `2 = - (u `2) ) by A2, A3, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
P1,P2,Q are_collinear by A4, COLLSP:4;
then A7: 0 = |{u,v,w}| by A1, BKMODEL1:1
.= (((((((u `1) * (- (u `2))) * 1) - ((1 * (- (u `2))) * (w `1))) - (((u `1) * 1) * (w `2))) + (((u `2) * 1) * (w `1))) - (((u `2) * (- (u `1))) * 1)) + ((1 * (- (u `1))) * (w `2)) by A6, ANPROJ_8:27
.= 2 * (((u `2) * (w `1)) - ((u `1) * (w `2))) ;
consider u9 being non zero Element of (TOP-REAL 3) such that
A8: ((u9 . 1) ^2) + ((u9 . 2) ^2) = 1 and
A9: u9 . 3 = 1 and
A10: P1 = Dir u9 by BKMODEL1:89;
A11: u = u9 by A9, A10, A1, A2, BKMODEL1:43;
( not u `1 = 0 or not u `2 = 0 )

proof

assume ( u `1 = 0 & u `2 = 0 ) ; :: thesis: contradiction
then ( u . 1 = 0 & u . 2 = 0 ) by EUCLID_5:def 1, EUCLID_5:def 2;
hence contradiction by A11, A8; :: thesis: verum

end;

then consider e being Real such that
A13: ( w `1 = e * (u `1) & w `2 = e * (u `2) ) by A7, BKMODEL1:2;
( w . 1 = e * (u `1) & w . 2 = e * (u `2) ) by A13, EUCLID_5:def 1, EUCLID_5:def 2;
then A14: ( w . 1 = e * (u . 1) & w . 2 = e * (u . 2) ) by EUCLID_5:def 1, EUCLID_5:def 2;

per cases ( e = 0 or e <> 0 ) ;

suppose e = 0 ; :: thesis: ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) )

hence ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) ) by A14; :: thesis: verum

end;

suppose e <> 0 ; :: thesis: ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) )

((w . 1) ^2) + ((w . 2) ^2) = ((w `1) * (w . 1)) + ((w . 2) * (w . 2)) by EUCLID_5:def 1
.= ((w `1) * (w `1)) + ((w . 2) * (w . 2)) by EUCLID_5:def 1
.= ((w `1) * (w `1)) + ((w `2) * (w . 2)) by EUCLID_5:def 2
.= ((w `1) * (w `1)) + ((w `2) * (w `2)) by EUCLID_5:def 2
.= (e * e) * (((u `1) * (u `1)) + ((u `2) * (u `2))) by A13
.= (e * e) * (((u . 1) * (u `1)) + ((u `2) * (u `2))) by EUCLID_5:def 1
.= (e * e) * (((u . 1) * (u . 1)) + ((u `2) * (u `2))) by EUCLID_5:def 1
.= (e * e) * (((u . 1) * (u . 1)) + ((u . 2) * (u `2))) by EUCLID_5:def 2
.= (e * e) * (((u . 1) * (u . 1)) + ((u . 2) * (u . 2))) by EUCLID_5:def 2
.= e * e by A8, A11 ;
then e ^2 < 1 by A1, A2, Th17;
then ( - 1 < e & e < 1 ) by SQUARE_1:52;
hence ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) ) by A14; :: thesis: verum

end;

end;