let P be non zero_proj3 Element of (ProjectiveSpace (TOP-REAL 3)); not P in Line ((Pdir3a P),(Pdir3b P))
assume
P in Line ((Pdir3a P),(Pdir3b P))
; 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; verum