let x, y, z be real number ; ( 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 y'',
z' being
Element of
REAL+ such that A8:
y = y''
and A9:
z = z'
and A10:
y'' <=' z'
by A2, A6, A7, XXREAL_0:def 5;
consider x',
y' being
Element of
REAL+ such that A11:
x = x'
and A12:
(
y = y' &
x' <=' y' )
by A1, A5, A6, XXREAL_0:def 5;
x' <=' z'
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 y'',
z' being
Element of
REAL+ such that A20:
y = [0 ,y'']
and A21:
z = [0 ,z']
and A22:
z' <=' y''
by A2, A18, A19, XXREAL_0:def 5;
consider x',
y' being
Element of
REAL+ such that A23:
x = [0 ,x']
and A24:
y = [0 ,y']
and A25:
y' <=' x'
by A1, A17, A18, XXREAL_0:def 5;
y' = y''
by A24, A20, ZFMISC_1:33;
then
z' <=' x'
by A25, A22, ARYTM_1:3;
hence
x <= z
by A17, A19, A23, A21, XXREAL_0:def 5;
verum end;