theorem Th25: :: ANPROJ10:41

for x, y, z being Element of (TOP-REAL 1) holds x,y,z are_collinear