let L be LINE of (IncProjSp_of real_projective_plane); 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)); 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); ( 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
; ( P <> Q & Dir |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| in L )
thus A7:
P <> Q
Dir |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| in Lproof
assume
P = Q
;
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;
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; verum