let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d, e, f being POINT of S st a,b <= c,d & c,d <= e,f holds
a,b <= e,f
let a, b, c, d, e, f be POINT of S; :: thesis: ( a,b <= c,d & c,d <= e,f implies a,b <= e,f )
assume A1: ( a,b <= c,d & c,d <= e,f ) ; :: thesis: a,b <= e,f
then consider x being POINT of S such that
A2: ( between a,b,x & a,x equiv c,d ) by Satz5p5;
consider y being POINT of S such that
A3: ( between c,d,y & c,y equiv e,f ) by A1, Satz5p5;
Collinear c,d,y by A3;
then consider q being POINT of S such that
A4: c,d,y cong a,x,q by A2, Satz2p2, Satz4p14;
A5: between a,b,q

proof

between a,x,q by A3, A4, Satz4p6;
hence between a,b,q by A2, Satz3p6p2; :: thesis: verum

end;

a,q equiv e,f

proof

a,q equiv c,y by A4, Satz2p2;
hence a,q equiv e,f by A3, Satz2p3; :: thesis: verum

end;

hence a,b <= e,f by A5, Satz5p5; :: thesis: verum