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

hereby :: thesis: R <> Q

assume R = P ; :: thesis: contradiction
then are_Prop u,w by A1, A3, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A7: u = a * w by ANPROJ_1:1;
A8: |[(u `1),(u `2),(u `3)]| = u by EUCLID_5:3
.= |[(a * (w `1)),(a * (w `2)),(a * (w `3))]| by A7, EUCLID_5:7 ;
then |[(u `1),(u `2),(u `3)]| = |[(a * (w `1)),(a * (w `2)),(a * (u `3))]| by A6, EUCLID_5:2;
then u `3 = a * (u `3) by FINSEQ_1:78;
then A9: a = 1 by A4, XCMPLX_1:7;
( w `1 = (u `1) + (v `1) & w `2 = (u `2) + (v `2) & w `3 = u `3 ) by A6, EUCLID_5:2;
then ( u `1 = (u `1) + (v `1) & u `2 = (u `2) + (v `2) ) by A8, A9, FINSEQ_1:78;
hence contradiction by A5, EUCLID_5:3, EUCLID_5:4; :: thesis: verum

end;

hereby :: thesis: verum

assume R = Q ; :: thesis: contradiction
then are_Prop v,w by A2, A3, ANPROJ_1:22;
then consider b being Real such that
A11: b <> 0 and
A12: v = b * w by ANPROJ_1:1;
|[(v `1),(v `2),(v `3)]| = v by EUCLID_5:3
.= |[(b * (w `1)),(b * (w `2)),(b * (w `3))]| by A12, EUCLID_5:7 ;
then |[(v `1),(v `2),(v `3)]| = |[(b * (w `1)),(b * (w `2)),(b * (u `3))]| by A6, EUCLID_5:2;
hence contradiction by A4, A11, A5, FINSEQ_1:78; :: thesis: verum

end;