theorem Th12: :: ANPROJ_8:14

for u, v, w being Point of (TOP-REAL 3) st ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) & a <> 0 ) holds
|{u,v,w}| = 0