let S be OAffinSpace; :: thesis: for x, y, z, t being Element of S st x,y,z are_collinear & x,y,t are_collinear holds
x,y '||' z,t
let x, y, z, t be Element of S; :: thesis: ( x,y,z are_collinear & x,y,t are_collinear implies x,y '||' z,t )
assume A1: ( x,y,z are_collinear & x,y,t are_collinear ) ; :: thesis: x,y '||' z,t

now :: thesis: ( x <> y implies x,y '||' z,t )

A2: ( x,y '||' x,z & x,y '||' x,t ) by A1;
assume x <> y ; :: thesis: x,y '||' z,t
then x,z '||' x,t by A2, Th23;
then z,x '||' z,t by Th21;
then x,z '||' z,t by Th22;
hence x,y '||' z,t by A2, Th23; :: thesis: verum

end;

hence x,y '||' z,t by Th20; :: thesis: verum