let CLSP be CollSp; for a, b, c being Point of CLSP st a,b,c are_collinear holds
( b,a,c are_collinear & a,c,b are_collinear )
let a, b, c be Point of CLSP; ( a,b,c are_collinear implies ( b,a,c are_collinear & a,c,b are_collinear ) )
assume A1:
a,b,c are_collinear
; ( b,a,c are_collinear & a,c,b are_collinear )
then
( a = b or ( a <> b & a,b,b are_collinear & a,b,a are_collinear & a,b,c are_collinear ) )
by Th2;
hence
b,a,c are_collinear
by Th2, Th3; a,c,b are_collinear
( a = b or ( a <> b & a,b,a are_collinear & a,b,c are_collinear & a,b,b are_collinear ) )
by A1, Th2;
hence
a,c,b are_collinear
by Th2, Th3; verum