let x, y, z be Real; ( x <= y & y <= z implies x <= z )
assume that
A1:
x <= y
and
A2:
y <= z
; x <= z
A3:
( x in REAL & y in REAL )
by XREAL_0:def 1;
A4:
z in REAL
by XREAL_0:def 1;
per cases
( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in [:{0},REAL+:] ) or ( y in REAL+ & z in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & z in REAL+ ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) )
by A3, A4, NUMBERS:def 1, XBOOLE_0:def 3;
suppose that A5:
x in REAL+
and A6:
y in REAL+
and A7:
z in REAL+
;
x <= zconsider y99,
z9 being
Element of
REAL+ such that A8:
y = y99
and A9:
z = z9
and A10:
y99 <=' z9
by A2, A6, A7, XXREAL_0:def 5;
consider x9,
y9 being
Element of
REAL+ such that A11:
x = x9
and A12:
(
y = y9 &
x9 <=' y9 )
by A1, A5, A6, XXREAL_0:def 5;
x9 <=' z9
by A12, A8, A10, ARYTM_1:3;
hence
x <= z
by A11, A9, XXREAL_0:def 5;
verum end; suppose that A17:
x in [:{0},REAL+:]
and A18:
y in [:{0},REAL+:]
and A19:
z in [:{0},REAL+:]
;
x <= zconsider y99,
z9 being
Element of
REAL+ such that A20:
y = [0,y99]
and A21:
z = [0,z9]
and A22:
z9 <=' y99
by A2, A18, A19, XXREAL_0:def 5;
consider x9,
y9 being
Element of
REAL+ such that A23:
x = [0,x9]
and A24:
y = [0,y9]
and A25:
y9 <=' x9
by A1, A17, A18, XXREAL_0:def 5;
y9 = y99
by A24, A20, XTUPLE_0:1;
then
z9 <=' x9
by A25, A22, ARYTM_1:3;
hence
x <= z
by A17, A19, A23, A21, XXREAL_0:def 5;
verum end;