let L be LINE of (IncProjSp_of real_projective_plane); :: thesis: for P being Element of (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3) st P = Dir u & P in L & u . 3 <> 0 holds
ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) ex v being non zero Element of (TOP-REAL 3) st
( Q = Dir v & Q in L & P <> Q & v . 3 <> 0 )
let P be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for u being non zero Element of (TOP-REAL 3) st P = Dir u & P in L & u . 3 <> 0 holds
ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) ex v being non zero Element of (TOP-REAL 3) st
( Q = Dir v & Q in L & P <> Q & v . 3 <> 0 )
let u be non zero Element of (TOP-REAL 3); :: thesis: ( P = Dir u & P in L & u . 3 <> 0 implies ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) ex v being non zero Element of (TOP-REAL 3) st
( Q = Dir v & Q in L & P <> Q & v . 3 <> 0 ) )
assume that
A1: P = Dir u and
A2: P in L and
A3: u . 3 <> 0 ; :: thesis: ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) ex v being non zero Element of (TOP-REAL 3) st
( Q = Dir v & Q in L & P <> Q & v . 3 <> 0 )
assume A4: for Q being Element of (ProjectiveSpace (TOP-REAL 3))
for v being non zero Element of (TOP-REAL 3) holds
( not Q = Dir v or not Q in L or not P <> Q or not v . 3 <> 0 ) ; :: thesis: contradiction
consider p, q being Element of (ProjectiveSpace (TOP-REAL 3)) such that
A5: p <> q and
A6: L = Line (p,q) by BKMODEL1:73;
consider up being Element of (TOP-REAL 3) such that
A7: not up is zero and
A8: p = Dir up by ANPROJ_1:26;
consider vp being Element of (TOP-REAL 3) such that
A9: not vp is zero and
A10: q = Dir vp by ANPROJ_1:26;
reconsider P9 = P as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
reconsider L9 = L as LINE of real_projective_plane by INCPROJ:4;

per cases ( ( up `3 = 0 & vp `3 = 0 ) or up `3 <> 0 or vp `3 <> 0 ) ;

suppose A11: ( up `3 = 0 & vp `3 = 0 ) ; :: thesis: contradiction

per cases ( P <> p or P <> q ) by A5;

suppose A12: P <> p ; :: thesis: contradiction

A13: u `3 <> 0 by A3, EUCLID_5:def 3;
not |[((u `1) + (up `1)),((u `2) + (up `2)),(u `3)]| is zero

proof

assume |[((u `1) + (up `1)),((u `2) + (up `2)),(u `3)]| is zero ; :: thesis: contradiction
then u `3 = 0 by EUCLID_5:4, FINSEQ_1:78;
hence contradiction by A3, EUCLID_5:def 3; :: thesis: verum

end;

then reconsider wp = |[((u `1) + (up `1)),((u `2) + (up `2)),(u `3)]| as non zero Element of (TOP-REAL 3) ;
reconsider R = Dir wp as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
A14: |{u,up,wp}| = 0 by A11, Th08;

now :: thesis: ( R <> P & R in L & wp . 3 <> 0 )

thus R <> P :: thesis: ( R in L & wp . 3 <> 0 )

proof

assume R = P ; :: thesis: contradiction
then are_Prop wp,u by A1, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A15: wp = a * u by ANPROJ_1:1;
( a = 1 & up `1 = 0 & up `2 = 0 )

proof

A16: |[(a * (u `1)),(a * (u `2)),(a * (u `3))]| = |[((u `1) + (up `1)),((u `2) + (up `2)),(u `3)]| by A15, EUCLID_5:7;
then ( a * (u `1) = (u `1) + (up `1) & a * (u `2) = (u `2) + (up `2) & a * (u `3) = u `3 ) by FINSEQ_1:78;
hence a = 1 by XCMPLX_1:7, A13; :: thesis: ( up `1 = 0 & up `2 = 0 )
then ( u `1 = (u `1) + (up `1) & u `2 = (u `2) + (up `2) ) by A16, FINSEQ_1:78;
hence ( up `1 = 0 & up `2 = 0 ) ; :: thesis: verum

end;

hence contradiction by A7, A11, EUCLID_5:3, EUCLID_5:4; :: thesis: verum

end;

reconsider R2 = R as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:2;

now :: thesis: ( R2 on L & L is LINE of real_projective_plane )

L = Line (P,p)

proof

( P in L & p in L & P <> p & L is LINE of real_projective_plane ) by A6, A2, A12, COLLSP:10, INCPROJ:4;
hence L = Line (P,p) by COLLSP:19; :: thesis: verum

end;

hence R2 on L by A1, A7, A8, A14, BKMODEL1:77; :: thesis: L is LINE of real_projective_plane
thus L is LINE of real_projective_plane by INCPROJ:4; :: thesis: verum

end;

hence R in L by INCPROJ:5; :: thesis: wp . 3 <> 0
thus wp . 3 <> 0 by A13; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum

end;

suppose A17: P <> q ; :: thesis: contradiction

A18: u `3 <> 0 by A3, EUCLID_5:def 3;
not |[((u `1) + (vp `1)),((u `2) + (vp `2)),(u `3)]| is zero

proof

assume |[((u `1) + (vp `1)),((u `2) + (vp `2)),(u `3)]| is zero ; :: thesis: contradiction
then u `3 = 0 by EUCLID_5:4, FINSEQ_1:78;
hence contradiction by A3, EUCLID_5:def 3; :: thesis: verum

end;

then reconsider wp = |[((u `1) + (vp `1)),((u `2) + (vp `2)),(u `3)]| as non zero Element of (TOP-REAL 3) ;
reconsider R = Dir wp as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
A19: |{u,vp,wp}| = 0 by A11, Th08;

now :: thesis: ( R <> P & R in L & wp . 3 <> 0 )

thus R <> P :: thesis: ( R in L & wp . 3 <> 0 )

proof

assume R = P ; :: thesis: contradiction
then are_Prop wp,u by A1, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A20: wp = a * u by ANPROJ_1:1;
( a = 1 & vp `1 = 0 & vp `2 = 0 )

proof

|[(a * (u `1)),(a * (u `2)),(a * (u `3))]| = |[((u `1) + (vp `1)),((u `2) + (vp `2)),(u `3)]| by A20, EUCLID_5:7;
then A21: ( a * (u `1) = (u `1) + (vp `1) & a * (u `2) = (u `2) + (vp `2) & a * (u `3) = u `3 ) by FINSEQ_1:78;
hence a = 1 by XCMPLX_1:7, A18; :: thesis: ( vp `1 = 0 & vp `2 = 0 )
hence ( vp `1 = 0 & vp `2 = 0 ) by A21; :: thesis: verum

end;

hence contradiction by A11, A9, EUCLID_5:3, EUCLID_5:4; :: thesis: verum

end;

reconsider R2 = R as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:2;

now :: thesis: ( R2 on L & L is LINE of real_projective_plane )

L = Line (P,q)

proof

( P in L & q in L & P <> q & L is LINE of real_projective_plane ) by A6, A2, COLLSP:10, A17, INCPROJ:4;
hence L = Line (P,q) by COLLSP:19; :: thesis: verum

end;

hence R2 on L by A1, A9, A10, A19, BKMODEL1:77; :: thesis: L is LINE of real_projective_plane
thus L is LINE of real_projective_plane by INCPROJ:4; :: thesis: verum

end;

hence R in L by INCPROJ:5; :: thesis: wp . 3 <> 0
thus wp . 3 <> 0 by A18; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum

end;

end;

end;

suppose ( up `3 <> 0 or vp `3 <> 0 ) ; :: thesis: contradiction

per cases then ( up `3 <> 0 or vp `3 <> 0 ) ;

suppose A22: up `3 <> 0 ; :: thesis: contradiction

per cases ( P = p or P <> p ) ;

suppose A23: P = p ; :: thesis: contradiction

per cases ( vp `3 <> 0 or vp `3 = 0 ) ;

suppose A24: vp `3 <> 0 ; :: thesis: contradiction

vp . 3 = 0 by A9, A10, A23, A5, A4, A6, COLLSP:10;
hence contradiction by A24, EUCLID_5:def 3; :: thesis: verum

end;

suppose A25: vp `3 = 0 ; :: thesis: contradiction

A26: u `3 <> 0 by A3, EUCLID_5:def 3;
not |[((u `1) + (vp `1)),((u `2) + (vp `2)),(u `3)]| is zero

proof

assume |[((u `1) + (vp `1)),((u `2) + (vp `2)),(u `3)]| is zero ; :: thesis: contradiction
then u `3 = 0 by EUCLID_5:4, FINSEQ_1:78;
hence contradiction by A3, EUCLID_5:def 3; :: thesis: verum

end;

then reconsider wp = |[((u `1) + (vp `1)),((u `2) + (vp `2)),(u `3)]| as non zero Element of (TOP-REAL 3) ;
reconsider R = Dir wp as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
A27: |{u,vp,wp}| = 0 by A25, Th08;

now :: thesis: ( R <> P & R in L & wp . 3 <> 0 )

thus R <> P :: thesis: ( R in L & wp . 3 <> 0 )

proof

assume R = P ; :: thesis: contradiction
then are_Prop wp,u by A1, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A28: wp = a * u by ANPROJ_1:1;
( a = 1 & vp `1 = 0 & vp `2 = 0 )

proof

|[(a * (u `1)),(a * (u `2)),(a * (u `3))]| = |[((u `1) + (vp `1)),((u `2) + (vp `2)),(u `3)]| by A28, EUCLID_5:7;
then A29: ( a * (u `1) = (u `1) + (vp `1) & a * (u `2) = (u `2) + (vp `2) & a * (u `3) = u `3 ) by FINSEQ_1:78;
hence a = 1 by XCMPLX_1:7, A26; :: thesis: ( vp `1 = 0 & vp `2 = 0 )
hence ( vp `1 = 0 & vp `2 = 0 ) by A29; :: thesis: verum

end;

hence contradiction by A25, EUCLID_5:3, EUCLID_5:4, A9; :: thesis: verum

end;

reconsider R2 = R as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:2;
( R2 on L & L is LINE of real_projective_plane ) by A6, A23, A1, A9, A10, A27, BKMODEL1:77, INCPROJ:4;
hence R in L by INCPROJ:5; :: thesis: wp . 3 <> 0
thus wp . 3 <> 0 by A26; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum

end;

end;

end;

suppose P <> p ; :: thesis: contradiction

then up . 3 = 0 by A8, A6, A4, A7, COLLSP:10;
hence contradiction by A22, EUCLID_5:def 3; :: thesis: verum

end;

end;

end;

suppose A30: vp `3 <> 0 ; :: thesis: contradiction

per cases ( P = q or P <> q ) ;

suppose A31: P = q ; :: thesis: contradiction

per cases ( up `3 <> 0 or up `3 = 0 ) ;

suppose A32: up `3 <> 0 ; :: thesis: contradiction

up . 3 = 0 by A7, A8, A31, A5, A4, A6, COLLSP:10;
hence contradiction by A32, EUCLID_5:def 3; :: thesis: verum

end;

suppose A33: up `3 = 0 ; :: thesis: contradiction

A34: u `3 <> 0 by A3, EUCLID_5:def 3;
not |[((u `1) + (up `1)),((u `2) + (up `2)),(u `3)]| is zero

proof

assume |[((u `1) + (up `1)),((u `2) + (up `2)),(u `3)]| is zero ; :: thesis: contradiction
then u `3 = 0 by EUCLID_5:4, FINSEQ_1:78;
hence contradiction by A3, EUCLID_5:def 3; :: thesis: verum

end;

then reconsider wp = |[((u `1) + (up `1)),((u `2) + (up `2)),(u `3)]| as non zero Element of (TOP-REAL 3) ;
reconsider R = Dir wp as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
A35: |{u,up,wp}| = 0 by A33, Th08;

now :: thesis: ( R <> P & R in L & wp . 3 <> 0 )

thus R <> P :: thesis: ( R in L & wp . 3 <> 0 )

proof

assume R = P ; :: thesis: contradiction
then are_Prop wp,u by A1, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A36: wp = a * u by ANPROJ_1:1;
( a = 1 & up `1 = 0 & up `2 = 0 )

proof

|[(a * (u `1)),(a * (u `2)),(a * (u `3))]| = |[((u `1) + (up `1)),((u `2) + (up `2)),(u `3)]| by A36, EUCLID_5:7;
then A37: ( a * (u `1) = (u `1) + (up `1) & a * (u `2) = (u `2) + (up `2) & a * (u `3) = u `3 ) by FINSEQ_1:78;
hence a = 1 by XCMPLX_1:7, A34; :: thesis: ( up `1 = 0 & up `2 = 0 )
hence ( up `1 = 0 & up `2 = 0 ) by A37; :: thesis: verum

end;

hence contradiction by A33, EUCLID_5:3, EUCLID_5:4, A7; :: thesis: verum

end;

reconsider R2 = R as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:2;

now :: thesis: ( R2 on L & L is LINE of real_projective_plane )

L = Line (P,p)

proof

( P in L & p in L & P <> p & L is LINE of real_projective_plane ) by A6, A31, A5, COLLSP:10, INCPROJ:4;
hence L = Line (P,p) by COLLSP:19; :: thesis: verum

end;

hence R2 on L by A1, A7, A8, A35, BKMODEL1:77; :: thesis: L is LINE of real_projective_plane
thus L is LINE of real_projective_plane by INCPROJ:4; :: thesis: verum

end;

hence R in L by INCPROJ:5; :: thesis: wp . 3 <> 0
thus wp . 3 <> 0 by A34; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum

end;

end;

end;

suppose P <> q ; :: thesis: contradiction

then vp . 3 = 0 by A10, A6, COLLSP:10, A4, A9;
hence contradiction by A30, EUCLID_5:def 3; :: thesis: verum

end;

end;

end;

end;

end;

end;