theorem Th01: :: BKMODEL1:1

for u, v, w being Element of (TOP-REAL 3)
for P1, P2, P3 being Element of (ProjectiveSpace (TOP-REAL 3)) st not u is zero & not v is zero & not w is zero & P1 = Dir u & P2 = Dir v & P3 = Dir w holds
( P1,P2,P3 are_collinear iff |{u,v,w}| = 0 )