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 )
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 ) )
assume x,y,z is_collinear ; :: thesis: ( x,z,y is_collinear & y,x,z is_collinear )
then x,y '||' x,z by Def5;
then ( x,z '||' x,y & y,x '||' y,z ) by Th26, Th27;
hence ( x,z,y is_collinear & y,x,z is_collinear ) by Def5; :: thesis: verum