let r, s, t be Real; :: 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 ) 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 ) or ( s in REAL+ & t in ) or ( r in & t in REAL+ ) or ( r in & s in & t in ) ) by ;
suppose that A5: r in REAL+ and
A6: s in REAL+ and
A7: t in REAL+ ; :: thesis: r <= t
consider s99, t9 being Element of REAL+ such that
A8: s = s99 and
A9: t = t9 and
A10: s99 <=' t9 by ;
consider x9, s9 being Element of REAL+ such that
A11: r = x9 and
A12: ( s = s9 & x9 <=' s9 ) by ;
x9 <=' t9 by ;
hence r <= t by A11, A9, Lm2; :: thesis: verum
end;
suppose A13: ( r in REAL+ & s in ) ; :: thesis: r <= t
then ( ( not r in REAL+ or not s in REAL+ ) & ( not r in or not s in ) ) by ;
hence r <= t by ; :: thesis: verum
end;
suppose A14: ( s in REAL+ & t in ) ; :: thesis: r <= t
then ( ( not t in REAL+ or not s in REAL+ ) & ( not t in or not s in ) ) by ;
hence r <= t by ; :: thesis: verum
end;
suppose that A15: r in and
A16: t in REAL+ ; :: thesis: r <= t
( ( not r in REAL+ or not t in REAL+ ) & ( not r in or not t in ) ) by ;
hence r <= t by ; :: thesis: verum
end;
suppose that A17: r in and
A18: s in and
A19: t in ; :: thesis: r <= t
consider s99, t9 being Element of REAL+ such that
A20: s = [0,s99] and
A21: t = [0,t9] and
A22: t9 <=' s99 by ;
consider x9, s9 being Element of REAL+ such that
A23: r = [0,x9] and
A24: s = [0,s9] and
A25: s9 <=' x9 by ;
s9 = s99 by ;
then t9 <=' x9 by ;
hence r <= t by A17, A19, A23, A21, Lm2; :: thesis: verum
end;
end;