theorem Th23:
for
P being
Point of
(ProjectiveSpace (TOP-REAL 3)) st not
Dir100 ,
Dir010 ,
P are_collinear & not
Dir100 ,
Dir001 ,
P are_collinear & not
Dir010 ,
Dir001 ,
P are_collinear holds
ex
a,
b,
c being non
zero Element of
F_Real st
P = Dir |[a,b,c]|