let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; ( a,b <= c,d & c,d <= e,f implies a,b <= e,f )
assume A1:
( a,b <= c,d & c,d <= e,f )
; 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
a,q equiv e,f
hence
a,b <= e,f
by A5, Satz5p5; verum