let x, y, z be Element of REAL+ ; :: thesis: ( x <=' y & y <=' z implies x <=' z )
assume x <=' y ; :: thesis: ( not y <=' z or x <=' z )
then consider z1 being Element of REAL+ such that
A1: x + z1 = y by ARYTM_2:9;
assume y <=' z ; :: thesis: x <=' z
then consider z2 being Element of REAL+ such that
A2: y + z2 = z by ARYTM_2:9;
z = x + (z1 + z2) by A1, A2, ARYTM_2:6;
hence x <=' z by ARYTM_2:19; :: thesis: verum