let SAS be Semi_Affine_Space; for a1, a2, a3 being Element of SAS st a1,a2,a3 is_collinear holds
( a1,a3,a2 is_collinear & a2,a1,a3 is_collinear & a2,a3,a1 is_collinear & a3,a1,a2 is_collinear & a3,a2,a1 is_collinear )
let a1, a2, a3 be Element of SAS; ( a1,a2,a3 is_collinear implies ( a1,a3,a2 is_collinear & a2,a1,a3 is_collinear & a2,a3,a1 is_collinear & a3,a1,a2 is_collinear & a3,a2,a1 is_collinear ) )
assume
a1,a2,a3 is_collinear
; ( a1,a3,a2 is_collinear & a2,a1,a3 is_collinear & a2,a3,a1 is_collinear & a3,a1,a2 is_collinear & a3,a2,a1 is_collinear )
then A1:
a1,a2 // a1,a3
by Def2;
then A2:
( a2,a3 // a2,a1 & a3,a2 // a3,a1 )
by Th18;
A3:
a3,a1 // a3,a2
by A1, Th18;
( a1,a3 // a1,a2 & a2,a1 // a2,a3 )
by A1, Th18;
hence
( a1,a3,a2 is_collinear & a2,a1,a3 is_collinear & a2,a3,a1 is_collinear & a3,a1,a2 is_collinear & a3,a2,a1 is_collinear )
by A2, A3, Def2; verum