let u, v, w be Element of (TOP-REAL 2); :: thesis: ( u,v,w are_collinear implies |[(u `1),(u `2),1]|,|[(v `1),(v `2),1]|,|[(w `1),(w `2),1]| are_collinear )
assume A1: u,v,w are_collinear ; :: thesis: |[(u `1),(u `2),1]|,|[(v `1),(v `2),1]|,|[(w `1),(w `2),1]| are_collinear
reconsider u1 = |[(u `1),(u `2),1]|, v1 = |[(v `1),(v `2),1]|, w1 = |[(w `1),(w `2),1]| as non zero Point of (TOP-REAL 3) ;
( u in LSeg (v,w) or v in LSeg (w,u) or w in LSeg (u,v) ) by A1, TOPREAL9:67;
then ( u1 in LSeg (v1,w1) or v1 in LSeg (w1,u1) or w1 in LSeg (u1,v1) ) by Th45;
hence |[(u `1),(u `2),1]|,|[(v `1),(v `2),1]|,|[(w `1),(w `2),1]| are_collinear by TOPREAL9:67; :: thesis: verum