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