let P be non zero_proj3 Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: not P in Line ((Pdir3a P),(Pdir3b P))
assume P in Line ((Pdir3a P),(Pdir3b P)) ; :: thesis: contradiction
then A1: Pdir3a P, Pdir3b P,P are_collinear by COLLSP:11;
reconsider u = normalize_proj3 P as non zero Element of (TOP-REAL 3) ;
A2: P = Dir u by Def6;
|{(dir3a P),(dir3b P),u}| = |(u,u)| by Th29;
then |(u,u)| = 0 by A2, A1, BKMODEL1:1;
hence contradiction by Th5; :: thesis: verum