let G be IncProjStr ; :: thesis: for a, b, c being POINT of G st a,b,c is_collinear holds
( a,c,b is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear & c,b,a is_collinear )
let a, b, c be POINT of G; :: thesis: ( a,b,c is_collinear implies ( a,c,b is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear & c,b,a is_collinear ) )
assume a,b,c is_collinear ; :: thesis: ( a,c,b is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear & c,b,a is_collinear )
then consider P being LINE of G such that
A1: {a,b,c} on P by Def5;
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 is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear & c,b,a is_collinear ) by A3, A2, Def5; :: thesis: verum