let G be IncProjStr ; :: thesis: for a, b, c being POINT of G st a,b,c are_collinear holds
( a,c,b are_collinear & b,a,c are_collinear & b,c,a are_collinear & c,a,b are_collinear & c,b,a are_collinear )
let a, b, c be POINT of G; :: thesis: ( a,b,c are_collinear implies ( a,c,b are_collinear & b,a,c are_collinear & b,c,a are_collinear & c,a,b are_collinear & c,b,a are_collinear ) )
assume a,b,c are_collinear ; :: thesis: ( a,c,b are_collinear & b,a,c are_collinear & b,c,a are_collinear & c,a,b are_collinear & c,b,a are_collinear )
then consider P being LINE of G such that
A1: {a,b,c} on P ;
A2: {c,b,a} on P by A1, Th1;
A3: ( {b,c,a} on P & {c,a,b} on P ) by A1, Th1;
( {a,c,b} on P & {b,a,c} on P ) by A1, Th1;
hence ( a,c,b are_collinear & b,a,c are_collinear & b,c,a are_collinear & c,a,b are_collinear & c,b,a are_collinear ) by A3, A2; :: thesis: verum