let r, s, t be Real; ( r <= s & s <= t implies r <= t )
assume that
A1:
r <= s
and
A2:
s <= t
; r <= t
A3:
( r in REAL & s in REAL )
by Def1;
A4:
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, A4, NUMBERS:def 1, XBOOLE_0:def 3;
suppose that A5:
r in REAL+
and A6:
s in REAL+
and A7:
t in REAL+
;
r <= tconsider s99,
t9 being
Element of
REAL+ such that A8:
s = s99
and A9:
t = t9
and A10:
s99 <=' t9
by A2, A6, A7, XXREAL_0:def 5;
consider x9,
s9 being
Element of
REAL+ such that A11:
r = x9
and A12:
(
s = s9 &
x9 <=' s9 )
by A1, A5, A6, XXREAL_0:def 5;
x9 <=' t9
by A12, A8, A10, ARYTM_1:3;
hence
r <= t
by A11, A9, Lm2;
verum end; suppose that A17:
r in [:{0},REAL+:]
and A18:
s in [:{0},REAL+:]
and A19:
t in [:{0},REAL+:]
;
r <= tconsider s99,
t9 being
Element of
REAL+ such that A20:
s = [0,s99]
and A21:
t = [0,t9]
and A22:
t9 <=' s99
by A2, A18, A19, XXREAL_0:def 5;
consider x9,
s9 being
Element of
REAL+ such that A23:
r = [0,x9]
and A24:
s = [0,s9]
and A25:
s9 <=' x9
by A1, A17, A18, XXREAL_0:def 5;
s9 = s99
by A24, A20, XTUPLE_0:1;
then
t9 <=' x9
by A25, A22, ARYTM_1:3;
hence
r <= t
by A17, A19, A23, A21, Lm2;
verum end; end;