let P be non zero_proj1 Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: not P in Line ((Pdir1a P),(Pdir1b P))
assume P in Line ((Pdir1a P),(Pdir1b P)) ; :: thesis: contradiction
then A1: Pdir1a P, Pdir1b P,P are_collinear by COLLSP:11;
reconsider u = normalize_proj1 P as non zero Element of (TOP-REAL 3) ;
A2: P = Dir u by Def2;
|{(dir1a P),(dir1b P),u}| = |(u,u)| by Th21;
then |(u,u)| = 0 by A2, A1, BKMODEL1:1;
hence contradiction by Th5; :: thesis: verum