theorem :: ANPROJ10:42
for T being RealLinearSpace st T = TOP-REAL 1 holds
for x, y, z being Element of T holds x,y,z are_collinear by Th25;