let S be OAffinSpace; :: thesis: for x, y being Element of S holds
( x,x,y is_collinear & x,y,y is_collinear & x,y,x is_collinear )
let x, y be Element of S; :: thesis: ( x,x,y is_collinear & x,y,y is_collinear & x,y,x is_collinear )
A1: x,y '||' x,x by Th25;
( x,x '||' x,y & x,y '||' x,y ) by Th24, Th25;
hence ( x,x,y is_collinear & x,y,y is_collinear & x,y,x is_collinear ) by A1, Def5; :: thesis: verum