let P be Element of BK_model ; :: thesis: for L being LINE of (IncProjSp_of real_projective_plane) st P in L holds
ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st
( P <> Q & Q in L & ( for u being non zero Element of (TOP-REAL 3) st Q = Dir u holds
u . 3 <> 0 ) )
let L be LINE of (IncProjSp_of real_projective_plane); :: thesis: ( P in L implies ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st
( P <> Q & Q in L & ( for u being non zero Element of (TOP-REAL 3) st Q = Dir u holds
u . 3 <> 0 ) ) )
assume A1: P in L ; :: thesis: ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st
( P <> Q & Q in L & ( for u being non zero Element of (TOP-REAL 3) st Q = Dir u holds
u . 3 <> 0 ) )
consider u being non zero Element of (TOP-REAL 3) such that
A2: ( P = Dir u & u . 3 = 1 ) and
BK_to_REAL2 P = |[(u . 1),(u . 2)]| by Def01;
consider Q being Element of (ProjectiveSpace (TOP-REAL 3)) such that
A3: ex v being non zero Element of (TOP-REAL 3) st
( Q = Dir v & Q in L & P <> Q & v . 3 <> 0 ) by A1, A2, Th09;
consider v being non zero Element of (TOP-REAL 3) such that
A4: ( Q = Dir v & Q in L & P <> Q & v . 3 <> 0 ) by A3;
take Q ; :: thesis: ( P <> Q & Q in L & ( for u being non zero Element of (TOP-REAL 3) st Q = Dir u holds
u . 3 <> 0 ) )

now :: thesis: ( P <> Q & Q in L & ( for u being non zero Element of (TOP-REAL 3) st Q = Dir u holds
u . 3 <> 0 ) )

thus ( P <> Q & Q in L ) by A3; :: thesis: for u being non zero Element of (TOP-REAL 3) st Q = Dir u holds
u . 3 <> 0
thus for u being non zero Element of (TOP-REAL 3) st Q = Dir u holds
u . 3 <> 0 :: thesis: verum

proof

let w be non zero Element of (TOP-REAL 3); :: thesis: ( Q = Dir w implies w . 3 <> 0 )
assume Q = Dir w ; :: thesis: w . 3 <> 0
then are_Prop v,w by A4, ANPROJ_1:22;
then consider a being Real such that
A5: a <> 0 and
A6: v = a * w by ANPROJ_1:1;
a * w = |[(a * (w `1)),(a * (w `2)),(a * (w `3))]| by EUCLID_5:7;
then v `3 = a * (w `3) by A6, EUCLID_5:2;
then w `3 = (v `3) / a by A5, XCMPLX_1:89
.= (v . 3) / a by EUCLID_5:def 3 ;
hence w . 3 <> 0 by A5, A4, EUCLID_5:def 3; :: thesis: verum

end;

end;

hence ( P <> Q & Q in L & ( for u being non zero Element of (TOP-REAL 3) st Q = Dir u holds
u . 3 <> 0 ) ) ; :: thesis: verum