let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( not P in BK_model \/ absolute implies ex l being LINE of (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute ) )
assume A1: not P in BK_model \/ absolute ; :: thesis: ex l being LINE of (IncProjSp_of real_projective_plane) 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 (TOP-REAL 3) 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 (IncProjSp_of real_projective_plane) 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 A6, EUCLID_5:def 1
.= |[0,0,(u9 `3)]| by A6, EUCLID_5:def 2
.= 0. (TOP-REAL 3) by A5, EUCLID_5:def 3, EUCLID_5:4 ;
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 (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute )

then reconsider v = |[(- (u9 . 2)),(u9 . 1),0]| as non zero Element of (TOP-REAL 3) ;
reconsider Q = Dir v as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
P <> Q

proof

assume P = Q ; :: thesis: contradiction
then are_Prop u9,v by A3, A4, ANPROJ_1:22;
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 A9, EUCLID_5:3 ;

now :: thesis: ( a * (- (u9 . 2)) = u9 . 1 & a * (u9 . 1) = u9 . 2 )

thus a * (- (u9 . 2)) = |[(u9 `1),(u9 `2),(u9 `3)]| `1 by A10, EUCLID_5:2
.= 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 A10, EUCLID_5:2
.= 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 A5, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
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 (IncProjSp_of real_projective_plane) 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 A11, XBOOLE_0:def 4;
reconsider R = R as Element of (ProjectiveSpace (TOP-REAL 3)) by A11;
consider w being non zero Element of (TOP-REAL 3) such that
A13: w . 3 = 1 and
A14: R = Dir w by A12, Th25;
reconsider R9 = R as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
reconsider l2 = l as LINE of (IncProjSp_of real_projective_plane) ;
A15: w `3 = 1 by A13, EUCLID_5:def 3;
A16: u9 `3 = 0 by A5, EUCLID_5:def 3;
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 A12, INCPROJ:5;
then |{u9,v,w}| = 0 by A3, A4, A14, BKMODEL1:77;
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 A15, ANPROJ_8:27
.= ((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 (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute )

then reconsider v = |[(- (u9 . 2)),(u9 . 1),0]| as non zero Element of (TOP-REAL 3) ;
reconsider Q = Dir v as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
P <> Q

proof

assume P = Q ; :: thesis: contradiction
then are_Prop u9,v by A3, A4, ANPROJ_1:22;
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 A22, EUCLID_5:3 ;

now :: thesis: ( a * (- (u9 . 2)) = u9 . 1 & a * (u9 . 1) = u9 . 2 )

thus a * (- (u9 . 2)) = |[(u9 `1),(u9 `2),(u9 `3)]| `1 by A23, EUCLID_5:2
.= 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 A23, EUCLID_5:2
.= 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 A5, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
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 (IncProjSp_of real_projective_plane) 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 A24, XBOOLE_0:def 4;
reconsider R = R as Element of (ProjectiveSpace (TOP-REAL 3)) by A24;
consider w being non zero Element of (TOP-REAL 3) such that
A26: w . 3 = 1 and
A27: R = Dir w by A25, Th25;
reconsider R9 = R as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
reconsider l2 = l as LINE of (IncProjSp_of real_projective_plane) ;
A28: w `3 = 1 by A26, EUCLID_5:def 3;
A29: u9 `3 = 0 by A5, EUCLID_5:def 3;
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 A25, INCPROJ:5;
then |{u9,v,w}| = 0 by A3, A4, A27, BKMODEL1:77;
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 A28, ANPROJ_8:27
.= ((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 (IncProjSp_of real_projective_plane) st
( P in l & l misses absolute )

reconsider u = |[((u9 . 1) / (u9 . 3)),((u9 . 2) / (u9 . 3)),1]| as non zero Element of (TOP-REAL 3) ;
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 A33, Th22
.= |[(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 A33, ANPROJ_1:1;
then A37: P = Dir u by A3, A4, ANPROJ_1:22;
( 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 (TOP-REAL 3) st not v is zero & P = Dir v holds
qfconic (1,1,(- 1),0,0,0,v) is negative

let v be Element of (TOP-REAL 3); :: 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 A36, A3, A4, ANPROJ_1:22;

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 A39, A40, BKMODEL1:81; :: 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 (IncProjSp_of real_projective_plane) 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 (TOP-REAL 3) ;
reconsider Q = Dir v as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
reconsider l9 = Line (P,Q) as LINE of real_projective_plane by Th26, A37, COLLSP:def 7;
reconsider l = l9 as Element of the Lines of (IncProjSp_of real_projective_plane) 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 A42, XBOOLE_0:def 4;
reconsider R = R as Element of (ProjectiveSpace (TOP-REAL 3)) by A42;
consider w being non zero Element of (TOP-REAL 3) such that
A44: w . 3 = 1 and
A45: R = Dir w by A43, Th25;
|[(w . 1),(w . 2)]| in circle (0,0,1) by A43, A44, A45, BKMODEL1:84;
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 A41, EUCLID_5:def 1; :: 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 A44, EUCLID_5:def 3; :: thesis: ( |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
reconsider R9 = R as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
reconsider l2 = l as LINE of (IncProjSp_of real_projective_plane) ;
R9 on l2 by A43, INCPROJ:5;
hence |{u,v,w}| = 0 by A37, A45, BKMODEL1:77; :: 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 (IncProjSp_of real_projective_plane) 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 (TOP-REAL 3) ;
reconsider Q = Dir v as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
reconsider l9 = Line (P,Q) as LINE of real_projective_plane by A37, Th26, COLLSP:def 7;
reconsider l = l9 as Element of the Lines of (IncProjSp_of real_projective_plane) 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 A48, XBOOLE_0:def 4;
reconsider R = R as Element of (ProjectiveSpace (TOP-REAL 3)) by A48;
consider w being non zero Element of (TOP-REAL 3) such that
A50: w . 3 = 1 and
A51: R = Dir w by A49, Th25;
|[(w . 1),(w . 2)]| in circle (0,0,1) by A49, A50, A51, BKMODEL1:84;
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 A47, EUCLID_5:def 2; :: 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 A50, EUCLID_5:def 3; :: thesis: ( |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) )
reconsider R9 = R as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
reconsider l2 = l as LINE of (IncProjSp_of real_projective_plane) ;
R9 on l2 by A49, INCPROJ:5;
hence |{u,v,w}| = 0 by A37, A51, BKMODEL1:77; :: 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;