for u, v, w being Element of (TOP-REAL 2) st u,v,w are_collinear holds
|[(u `1),(u `2),1]|,|[(v `1),(v `2),1]|,|[(w `1),(w `2),1]| are_collinear