let SAS be Semi_Affine_Space; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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,a2 // a1,a3 by Def2;
then ( a1,a3 // a1,a2 & a2,a1 // a2,a3 & a2,a3 // a2,a1 & a3,a2 // a3,a1 & a3,a1 // a3,a2 ) by 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 Def2; :: thesis: verum