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;

( 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 )
;

end;

suppose A5:
u9 . 3 = 0
; :: thesis: ex l being LINE of (IncProjSp_of real_projective_plane) st

( P in l & l misses absolute )

( P in l & l misses absolute )

( u9 . 1 <> 0 or u9 . 2 <> 0 )

end;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;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

per cases then
( u9 . 1 <> 0 or u9 . 2 <> 0 )
;

end;

suppose A7:
u9 . 1 <> 0
; :: thesis: ex l being LINE of (IncProjSp_of real_projective_plane) st

( P in l & l misses absolute )

( 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

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

end;reconsider Q = Dir v as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;

P <> Q

proof

then reconsider l9 = Line (P,Q) as LINE of real_projective_plane by COLLSP:def 7;
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 ;

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 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 )

then
( u9 . 1 = 0 & u9 . 2 = 0 )
by Th10;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;.= 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

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

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

hence
( P in l & l misses absolute )
by COLLSP:10; :: thesis: verum
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;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

suppose A20:
u9 . 2 <> 0
; :: thesis: ex l being LINE of (IncProjSp_of real_projective_plane) st

( P in l & l misses absolute )

( 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

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

end;reconsider Q = Dir v as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;

P <> Q

proof

then reconsider l9 = Line (P,Q) as LINE of real_projective_plane by COLLSP:def 7;
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 ;

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 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 )

then
( u9 . 1 = 0 & u9 . 2 = 0 )
by Th10;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;.= 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

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

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

hence
( P in l & l misses absolute )
by COLLSP:10; :: thesis: verum
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;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

suppose A33:
u9 . 3 <> 0
; :: thesis: ex l being LINE of (IncProjSp_of real_projective_plane) st

( P in l & l misses absolute )

( 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 )

end;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

end;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

hence
contradiction
by A2, BKMODEL2:def 1; :: thesis: verumqfconic (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;

end;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) )

hence
qfconic (1,1,(- 1),0,0,0,v) is negative
by A39, A40, BKMODEL1:81; :: thesis: verumthus
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;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

per cases then
( u . 1 <> 0 or u . 2 <> 0 )
;

end;

suppose A41:
u . 1 <> 0
; :: thesis: ex l being LINE of (IncProjSp_of real_projective_plane) st

( P in l & l misses absolute )

( 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

end;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

hence
( P in l & l misses absolute )
by COLLSP:10; :: thesis: verum
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;

end;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) )

hence
contradiction
by A46, Th23; :: thesis: verumthus
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

end;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

suppose A47:
u . 2 <> 0
; :: thesis: ex l being LINE of (IncProjSp_of real_projective_plane) st

( P in l & l misses absolute )

( 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

end;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

hence
( P in l & l misses absolute )
by COLLSP:10; :: thesis: verum
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;

end;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) )

hence
contradiction
by A53, Th24; :: thesis: verumthus
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

end;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