let r, s, t be real number ; :: thesis: ( r <= s & s <= t implies r <= t )
assume that
A1:
r <= s
and
A2:
s <= t
; :: thesis: r <= t
A3:
( r in REAL & s in REAL & t in REAL )
by Def1;
per cases
( ( r in REAL+ & s in REAL+ & t in REAL+ ) or ( r in REAL+ & s in [:{0 },REAL+ :] ) or ( s in REAL+ & t in [:{0 },REAL+ :] ) or ( r in [:{0 },REAL+ :] & t in REAL+ ) or ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] & t in [:{0 },REAL+ :] ) )
by A3, NUMBERS:def 1, XBOOLE_0:def 3;
suppose that A4:
r in REAL+
and A5:
s in REAL+
and A6:
t in REAL+
;
:: thesis: r <= tconsider x',
s' being
Element of
REAL+ such that A7:
r = x'
and A8:
s = s'
and A9:
x' <=' s'
by A1, A4, A5, XXREAL_0:def 5;
consider s'',
t' being
Element of
REAL+ such that A10:
s = s''
and A11:
t = t'
and A12:
s'' <=' t'
by A2, A5, A6, XXREAL_0:def 5;
x' <=' t'
by A8, A9, A10, A12, ARYTM_1:3;
hence
r <= t
by A7, A11, Lm2;
:: thesis: verum end; suppose that A17:
r in [:{0 },REAL+ :]
and A18:
s in [:{0 },REAL+ :]
and A19:
t in [:{0 },REAL+ :]
;
:: thesis: r <= tconsider x',
s' being
Element of
REAL+ such that A20:
r = [0 ,x']
and A21:
s = [0 ,s']
and A22:
s' <=' x'
by A1, A17, A18, XXREAL_0:def 5;
consider s'',
t' being
Element of
REAL+ such that A23:
s = [0 ,s'']
and A24:
t = [0 ,t']
and A25:
t' <=' s''
by A2, A18, A19, XXREAL_0:def 5;
s' = s''
by A21, A23, ZFMISC_1:33;
then
t' <=' x'
by A22, A25, ARYTM_1:3;
hence
r <= t
by A17, A19, A20, A24, Lm2;
:: thesis: verum end;