let P be Point of (); :: thesis: ( not P in BK_model \/ absolute implies ex l being LINE of st
( P in l & l misses absolute ) )

assume A1: not P in BK_model \/ absolute ; :: thesis: ex l being LINE of st
( P in l & l misses absolute )

then A2: ( not P in BK_model & not P in absolute ) by XBOOLE_0:def 3;
consider u9 being Element of () such that
A3: not u9 is zero and
A4: P = Dir u9 by ANPROJ_1:26;
per cases ( u9 . 3 = 0 or u9 . 3 <> 0 ) ;
suppose A5: u9 . 3 = 0 ; :: thesis: ex l being LINE of st
( P in l & l misses absolute )

( u9 . 1 <> 0 or u9 . 2 <> 0 )
proof
assume A6: ( u9 . 1 = 0 & u9 . 2 = 0 ) ; :: thesis: contradiction
u9 = |[(u9 `1),(u9 `2),(u9 `3)]| by EUCLID_5:3
.= |[0,(u9 `2),(u9 `3)]| by
.= |[0,0,(u9 `3)]| by
.= 0. () by ;
hence contradiction by A3; :: thesis: verum
end;
per cases then ( u9 . 1 <> 0 or u9 . 2 <> 0 ) ;
suppose A7: u9 . 1 <> 0 ; :: thesis: ex l being LINE of st
( P in l & l misses absolute )

then reconsider v = |[(- (u9 . 2)),(u9 . 1),0]| as non zero Element of () ;
reconsider Q = Dir v as Point of () by ANPROJ_1:26;
P <> Q
proof
assume P = Q ; :: thesis: contradiction
then are_Prop u9,v by ;
then consider a being Real such that
a <> 0 and
A9: u9 = a * v by ANPROJ_1:1;
A10: |[(a * (- (u9 . 2))),(a * (u9 . 1)),(a * 0)]| = a * v by EUCLID_5:8
.= |[(u9 `1),(u9 `2),(u9 `3)]| by ;
now :: thesis: ( a * (- (u9 . 2)) = u9 . 1 & a * (u9 . 1) = u9 . 2 )
thus a * (- (u9 . 2)) = |[(u9 `1),(u9 `2),(u9 `3)]| `1 by
.= u9 `1 by EUCLID_5:2
.= u9 . 1 by EUCLID_5:def 1 ; :: thesis: a * (u9 . 1) = u9 . 2
thus a * (u9 . 1) = |[(u9 `1),(u9 `2),(u9 `3)]| `2 by
.= u9 `2 by EUCLID_5:2
.= u9 . 2 by EUCLID_5:def 2 ; :: thesis: verum
end;
then ( u9 . 1 = 0 & u9 . 2 = 0 ) by Th10;
then ( u9 `1 = 0 & u9 `2 = 0 & u9 `3 = 0 ) by ;
hence contradiction by A3, EUCLID_5:3, EUCLID_5:4; :: thesis: verum
end;
then reconsider l9 = Line (P,Q) as LINE of real_projective_plane by COLLSP:def 7;
reconsider l = l9 as Element of the Lines of by INCPROJ:4;
take l ; :: thesis: ( P in l & l misses absolute )
l misses absolute
proof
assume not l misses absolute ; :: thesis: contradiction
then consider R being object such that
A11: R in l /\ absolute by XBOOLE_0:7;
A12: ( R in l & R in absolute ) by ;
reconsider R = R as Element of () by A11;
consider w being non zero Element of () such that
A13: w . 3 = 1 and
A14: R = Dir w by ;
reconsider R9 = R as POINT of by INCPROJ:3;
reconsider l2 = l as LINE of ;
A15: w `3 = 1 by ;
A16: u9 `3 = 0 by ;
A17: v `1 = - (u9 . 2) by EUCLID_5:2
.= - (u9 `2) by EUCLID_5:def 2 ;
A18: v `2 = u9 . 1 by EUCLID_5:2
.= u9 `1 by EUCLID_5:def 1 ;
A19: v `3 = 0 by EUCLID_5:2;
R9 on l2 by ;
then |{u9,v,w}| = 0 by ;
then 0 = (((((((u9 `1) * (v `2)) * 1) - (((u9 `3) * (v `2)) * (w `1))) - (((u9 `1) * (v `3)) * (w `2))) + (((u9 `2) * (v `3)) * (w `1))) - (((u9 `2) * (v `1)) * 1)) + (((u9 `3) * (v `1)) * (w `2)) by
.= ((u9 `1) ^2) + ((u9 `2) ^2) by A16, A17, A18, A19 ;
then ( u9 `1 = 0 & u9 `2 = 0 ) ;
hence contradiction by A7, EUCLID_5:def 1; :: thesis: verum
end;
hence ( P in l & l misses absolute ) by COLLSP:10; :: thesis: verum
end;
suppose A20: u9 . 2 <> 0 ; :: thesis: ex l being LINE of st
( P in l & l misses absolute )

then reconsider v = |[(- (u9 . 2)),(u9 . 1),0]| as non zero Element of () ;
reconsider Q = Dir v as Point of () by ANPROJ_1:26;
P <> Q
proof
assume P = Q ; :: thesis: contradiction
then are_Prop u9,v by ;
then consider a being Real such that
a <> 0 and
A22: u9 = a * v by ANPROJ_1:1;
A23: |[(a * (- (u9 . 2))),(a * (u9 . 1)),(a * 0)]| = a * v by EUCLID_5:8
.= |[(u9 `1),(u9 `2),(u9 `3)]| by ;
now :: thesis: ( a * (- (u9 . 2)) = u9 . 1 & a * (u9 . 1) = u9 . 2 )
thus a * (- (u9 . 2)) = |[(u9 `1),(u9 `2),(u9 `3)]| `1 by
.= u9 `1 by EUCLID_5:2
.= u9 . 1 by EUCLID_5:def 1 ; :: thesis: a * (u9 . 1) = u9 . 2
thus a * (u9 . 1) = |[(u9 `1),(u9 `2),(u9 `3)]| `2 by
.= u9 `2 by EUCLID_5:2
.= u9 . 2 by EUCLID_5:def 2 ; :: thesis: verum
end;
then ( u9 . 1 = 0 & u9 . 2 = 0 ) by Th10;
then ( u9 `1 = 0 & u9 `2 = 0 & u9 `3 = 0 ) by ;
hence contradiction by A3, EUCLID_5:3, EUCLID_5:4; :: thesis: verum
end;
then reconsider l9 = Line (P,Q) as LINE of real_projective_plane by COLLSP:def 7;
reconsider l = l9 as Element of the Lines of by INCPROJ:4;
take l ; :: thesis: ( P in l & l misses absolute )
l misses absolute
proof
assume not l misses absolute ; :: thesis: contradiction
then consider R being object such that
A24: R in l /\ absolute by XBOOLE_0:7;
A25: ( R in l & R in absolute ) by ;
reconsider R = R as Element of () by A24;
consider w being non zero Element of () such that
A26: w . 3 = 1 and
A27: R = Dir w by ;
reconsider R9 = R as POINT of by INCPROJ:3;
reconsider l2 = l as LINE of ;
A28: w `3 = 1 by ;
A29: u9 `3 = 0 by ;
A30: v `1 = - (u9 . 2) by EUCLID_5:2
.= - (u9 `2) by EUCLID_5:def 2 ;
A31: v `2 = u9 . 1 by EUCLID_5:2
.= u9 `1 by EUCLID_5:def 1 ;
A32: v `3 = 0 by EUCLID_5:2;
R9 on l2 by ;
then |{u9,v,w}| = 0 by ;
then 0 = (((((((u9 `1) * (v `2)) * 1) - (((u9 `3) * (v `2)) * (w `1))) - (((u9 `1) * (v `3)) * (w `2))) + (((u9 `2) * (v `3)) * (w `1))) - (((u9 `2) * (v `1)) * 1)) + (((u9 `3) * (v `1)) * (w `2)) by
.= ((u9 `1) ^2) + ((u9 `2) ^2) by A29, A30, A31, A32 ;
then ( u9 `1 = 0 & u9 `2 = 0 ) ;
hence contradiction by A20, EUCLID_5:def 2; :: thesis: verum
end;
hence ( P in l & l misses absolute ) by COLLSP:10; :: thesis: verum
end;
end;
end;
suppose A33: u9 . 3 <> 0 ; :: thesis: ex l being LINE of st
( P in l & l misses absolute )

reconsider u = |[((u9 . 1) / (u9 . 3)),((u9 . 2) / (u9 . 3)),1]| as non zero Element of () ;
A34: u `3 = 1 by EUCLID_5:2;
then A35: u . 3 = 1 by EUCLID_5:def 3;
(u9 . 3) * u = |[(u9 . 1),(u9 . 2),(u9 . 3)]| by
.= |[(u9 `1),(u9 . 2),(u9 . 3)]| by EUCLID_5:def 1
.= |[(u9 `1),(u9 `2),(u9 . 3)]| by EUCLID_5:def 2
.= |[(u9 `1),(u9 `2),(u9 `3)]| by EUCLID_5:def 3
.= u9 by EUCLID_5:3 ;
then A36: are_Prop u,u9 by ;
then A37: P = Dir u by ;
( u . 1 <> 0 or u . 2 <> 0 )
proof
assume A38: ( u . 1 = 0 & u . 2 = 0 ) ; :: thesis: contradiction
now :: thesis: for v being Element of () st not v is zero & P = Dir v holds
qfconic (1,1,(- 1),0,0,0,v) is negative
let v be Element of (); :: thesis: ( not v is zero & P = Dir v implies qfconic (1,1,(- 1),0,0,0,v) is negative )
assume A39: not v is zero ; :: thesis: ( P = Dir v implies qfconic (1,1,(- 1),0,0,0,v) is negative )
assume P = Dir v ; :: thesis: qfconic (1,1,(- 1),0,0,0,v) is negative
then A40: Dir u = Dir v by ;
now :: thesis: ( 0 < (u . 3) ^2 & qfconic (1,1,(- 1),0,0,0,u) = (- 1) * ((u . 3) ^2) )
thus 0 < (u . 3) ^2 by A35; :: thesis: qfconic (1,1,(- 1),0,0,0,u) = (- 1) * ((u . 3) ^2)
thus qfconic (1,1,(- 1),0,0,0,u) = ((((((1 * (u . 1)) * (u . 1)) + ((1 * (u . 2)) * (u . 2))) + (((- 1) * (u . 3)) * (u . 3))) + ((0 * (u . 1)) * (u . 2))) + ((0 * (u . 1)) * (u . 3))) + ((0 * (u . 2)) * (u . 3)) by PASCAL:def 1
.= (- 1) * ((u . 3) ^2) by A38 ; :: thesis: verum
end;
hence qfconic (1,1,(- 1),0,0,0,v) is negative by ; :: thesis: verum
end;
hence contradiction by A2, BKMODEL2:def 1; :: thesis: verum
end;
per cases then ( u . 1 <> 0 or u . 2 <> 0 ) ;
suppose A41: u . 1 <> 0 ; :: thesis: ex l being LINE of st
( P in l & l misses absolute )

then reconsider u1 = u . 1 as non zero Real ;
reconsider u2 = u . 2 as Real ;
reconsider v = |[(- u2),u1,0]| as non zero Element of () ;
reconsider Q = Dir v as Element of () by ANPROJ_1:26;
reconsider l9 = Line (P,Q) as LINE of real_projective_plane by ;
reconsider l = l9 as Element of the Lines of by INCPROJ:4;
take l ; :: thesis: ( P in l & l misses absolute )
l misses absolute
proof
assume not l misses absolute ; :: thesis: contradiction
then consider R being object such that
A42: R in l /\ absolute by XBOOLE_0:7;
A43: ( R in l & R in absolute ) by ;
reconsider R = R as Element of () by A42;
consider w being non zero Element of () such that
A44: w . 3 = 1 and
A45: R = Dir w by ;
|[(w . 1),(w . 2)]| in circle (0,0,1) by ;
then ((w . 1) ^2) + ((w . 2) ^2) = 1 by BKMODEL1:13;
then ((w `1) ^2) + ((w . 2) ^2) = 1 by EUCLID_5:def 1;
then A46: ((w `1) ^2) + ((w `2) ^2) = 1 by EUCLID_5:def 2;
now :: thesis: ( u `1 <> 0 & u `3 = 1 & v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
thus u `1 <> 0 by ; :: thesis: ( u `3 = 1 & v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
thus u `3 = 1 by EUCLID_5:2; :: thesis: ( v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
v `1 = - u2 by EUCLID_5:2;
hence v `1 = - (u `2) by EUCLID_5:def 2; :: thesis: ( v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
v `2 = u . 1 by EUCLID_5:2;
hence v `2 = u `1 by EUCLID_5:def 1; :: thesis: ( v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
thus v `3 = 0 by EUCLID_5:2; :: thesis: ( w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
thus w `3 = 1 by ; :: thesis: ( |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
reconsider R9 = R as POINT of by INCPROJ:3;
reconsider l2 = l as LINE of ;
R9 on l2 by ;
hence |{u,v,w}| = 0 by ; :: thesis: 1 < ((u `1) ^2) + ((u `2) ^2)
thus 1 < ((u `1) ^2) + ((u `2) ^2) :: thesis: verum
proof
assume not 1 < ((u `1) ^2) + ((u `2) ^2) ; :: thesis: contradiction
then Dir |[(u `1),(u `2),1]| in BK_model \/ absolute by Th28;
hence contradiction by A37, A1, A34, EUCLID_5:3; :: thesis: verum
end;
end;
hence contradiction by A46, Th23; :: thesis: verum
end;
hence ( P in l & l misses absolute ) by COLLSP:10; :: thesis: verum
end;
suppose A47: u . 2 <> 0 ; :: thesis: ex l being LINE of st
( P in l & l misses absolute )

then reconsider u2 = u . 2 as non zero Real ;
reconsider u1 = u . 1 as Real ;
reconsider v = |[(- u2),u1,0]| as non zero Element of () ;
reconsider Q = Dir v as Element of () by ANPROJ_1:26;
reconsider l9 = Line (P,Q) as LINE of real_projective_plane by ;
reconsider l = l9 as Element of the Lines of by INCPROJ:4;
take l ; :: thesis: ( P in l & l misses absolute )
l misses absolute
proof
assume l meets absolute ; :: thesis: contradiction
then consider R being object such that
A48: R in l /\ absolute by XBOOLE_0:7;
A49: ( R in l & R in absolute ) by ;
reconsider R = R as Element of () by A48;
consider w being non zero Element of () such that
A50: w . 3 = 1 and
A51: R = Dir w by ;
|[(w . 1),(w . 2)]| in circle (0,0,1) by ;
then ((w . 1) ^2) + ((w . 2) ^2) = 1 by BKMODEL1:13;
then ((w `1) ^2) + ((w . 2) ^2) = 1 by EUCLID_5:def 1;
then A53: ((w `1) ^2) + ((w `2) ^2) = 1 by EUCLID_5:def 2;
now :: thesis: ( u `2 <> 0 & u `3 = 1 & v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
thus u `2 <> 0 by ; :: thesis: ( u `3 = 1 & v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
thus u `3 = 1 by EUCLID_5:2; :: thesis: ( v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
v `1 = - u2 by EUCLID_5:2;
hence v `1 = - (u `2) by EUCLID_5:def 2; :: thesis: ( v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
v `2 = u . 1 by EUCLID_5:2;
hence v `2 = u `1 by EUCLID_5:def 1; :: thesis: ( v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
thus v `3 = 0 by EUCLID_5:2; :: thesis: ( w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
thus w `3 = 1 by ; :: thesis: ( |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
reconsider R9 = R as POINT of by INCPROJ:3;
reconsider l2 = l as LINE of ;
R9 on l2 by ;
hence |{u,v,w}| = 0 by ; :: thesis: 1 < ((u `1) ^2) + ((u `2) ^2)
thus 1 < ((u `1) ^2) + ((u `2) ^2) :: thesis: verum
proof
assume not 1 < ((u `1) ^2) + ((u `2) ^2) ; :: thesis: contradiction
then Dir |[(u `1),(u `2),1]| in BK_model \/ absolute by Th28;
hence contradiction by A37, A1, EUCLID_5:3, A34; :: thesis: verum
end;
end;
hence contradiction by A53, Th24; :: thesis: verum
end;
hence ( P in l & l misses absolute ) by COLLSP:10; :: thesis: verum
end;
end;
end;
end;