let L be LINE of (IncProjSp_of real_projective_plane); :: thesis: for P, Q being Element of (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3) st P in L & Q in L & P = Dir u & Q = Dir v & u `3 <> 0 & v `3 = 0 holds
( P <> Q & Dir |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| in L )
let P, Q be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for u, v being non zero Element of (TOP-REAL 3) st P in L & Q in L & P = Dir u & Q = Dir v & u `3 <> 0 & v `3 = 0 holds
( P <> Q & Dir |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| in L )
let u, v be non zero Element of (TOP-REAL 3); :: thesis: ( P in L & Q in L & P = Dir u & Q = Dir v & u `3 <> 0 & v `3 = 0 implies ( P <> Q & Dir |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| in L ) )
assume that
A1: P in L and
A2: Q in L and
A3: P = Dir u and
A4: Q = Dir v and
A5: u `3 <> 0 and
A6: v `3 = 0 ; :: thesis: ( P <> Q & Dir |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| in L )
thus A7: P <> Q :: thesis: Dir |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| in L

proof

assume P = Q ; :: thesis: contradiction
then A8: are_Prop u,v by A3, A4, ANPROJ_1:22;
( u = |[(u `1),(u `2),(u `3)]| & v = |[(v `1),(v `2),0]| ) by A6, EUCLID_5:3;
hence contradiction by A5, A8, Th06; :: thesis: verum

end;

reconsider w = |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| as non zero Element of (TOP-REAL 3) by A5, Th05;
reconsider R = Dir w as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
( u = |[(u `1),(u `2),(u `3)]| & v = |[(v `1),(v `2),0]| ) by A6, EUCLID_5:3;
then |{u,v,w}| = 0 by Th04;
then P,Q,R are_collinear by A3, A4, BKMODEL1:1;
then R in Line (P,Q) by COLLSP:11;
hence Dir |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| in L by A1, A2, A7, Th07; :: thesis: verum