for SAS being Semi_Affine_Space
for a1, a2, a3 being Element of SAS st a1,a2,a3 are_collinear holds
( a1,a3,a2 are_collinear & a2,a1,a3 are_collinear & a2,a3,a1 are_collinear & a3,a1,a2 are_collinear & a3,a2,a1 are_collinear ) by Th7;