let S be OAffinSpace; :: thesis: for x, y, z being Element of S st x,y,z are_collinear holds
( x,z,y are_collinear & y,x,z are_collinear & y,z,x are_collinear & z,x,y are_collinear & z,y,x are_collinear )
let x, y, z be Element of S; :: thesis: ( x,y,z are_collinear implies ( x,z,y are_collinear & y,x,z are_collinear & y,z,x are_collinear & z,x,y are_collinear & z,y,x are_collinear ) )
assume x,y,z are_collinear ; :: thesis: ( x,z,y are_collinear & y,x,z are_collinear & y,z,x are_collinear & z,x,y are_collinear & z,y,x are_collinear )
hence ( x,z,y are_collinear & y,x,z are_collinear ) by Lm3; :: thesis: ( y,z,x are_collinear & z,x,y are_collinear & z,y,x are_collinear )
hence ( y,z,x are_collinear & z,x,y are_collinear ) by Lm3; :: thesis: z,y,x are_collinear
hence z,y,x are_collinear by Lm3; :: thesis: verum