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