let P be non zero_proj2 Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: not P in Line ((Pdir2a P),(Pdir2b P))
assume P in Line ((Pdir2a P),(Pdir2b P)) ; :: thesis: contradiction
then A1: Pdir2a P, Pdir2b P,P are_collinear by COLLSP:11;
reconsider u = normalize_proj2 P as non zero Element of (TOP-REAL 3) ;
A2: P = Dir u by Def4;
|{(dir2a P),(dir2b P),u}| = - |(u,u)| by Th25;
then |(u,u)| = 0 by A2, A1, BKMODEL1:1;
hence contradiction by Th5; :: thesis: verum