let G be IncProjStr ; 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; ( 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
; ( 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; verum