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