let a, b be ext-real number ; :: thesis: ( a <= b & b <= a implies a = b )
assume that
A1: a <= b and
A2: b <= a ; :: thesis: a = b

per cases ( ( a in REAL+ & b in REAL+ ) or ( a in REAL+ & b in [:{0 },REAL+ :] ) or ( b in REAL+ & a in [:{0 },REAL+ :] ) or ( a in [:{0 },REAL+ :] & b in [:{0 },REAL+ :] ) or ( ( a = -infty or a = +infty ) & ( b = -infty or b = +infty ) ) or ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0 },REAL+ :] or not b in [:{0 },REAL+ :] ) & ( not b in REAL+ or not a in [:{0 },REAL+ :] ) & ( not a in REAL+ or not b in [:{0 },REAL+ :] ) ) ) ;

suppose ( a in REAL+ & b in REAL+ ) ; :: thesis: a = b

then ( ex a9, b9 being Element of REAL+ st
( a = a9 & b = b9 & a9 <=' b9 ) & ex b99, a99 being Element of REAL+ st
( b = b99 & a = a99 & b99 <=' a99 ) ) by A1, A2, Def5;
hence a = b by ARYTM_1:4; :: thesis: verum

end;

suppose A3: ( a in REAL+ & b in [:{0 },REAL+ :] ) ; :: thesis: a = b

then ( not b in REAL+ & not a in [:{0 },REAL+ :] ) by ARYTM_0:5, XBOOLE_0:3;
hence a = b by A1, A3, Def5, Lm3, Lm4; :: thesis: verum

end;

suppose A4: ( b in REAL+ & a in [:{0 },REAL+ :] ) ; :: thesis: a = b

then ( not a in REAL+ & not b in [:{0 },REAL+ :] ) by ARYTM_0:5, XBOOLE_0:3;
hence a = b by A2, A4, Def5, Lm3, Lm4; :: thesis: verum

end;

suppose A5: ( a in [:{0 },REAL+ :] & b in [:{0 },REAL+ :] ) ; :: thesis: a = b

consider a9, b9 being Element of REAL+ such that
A6: ( a = [0 ,a9] & b = [0 ,b9] ) and
A7: b9 <=' a9 by A1, A5, Def5;
consider b99, a99 being Element of REAL+ such that
A8: ( b = [0 ,b99] & a = [0 ,a99] ) and
A9: a99 <=' b99 by A2, A5, Def5;
( a9 = a99 & b9 = b99 ) by A6, A8, ZFMISC_1:33;
hence a = b by A7, A8, A9, ARYTM_1:4; :: thesis: verum

end;

suppose ( ( a = -infty or a = +infty ) & ( b = -infty or b = +infty ) ) ; :: thesis: a = b

hence a = b by A1, A2, Lm6; :: thesis: verum

end;

suppose that A10: ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0 },REAL+ :] or not b in [:{0 },REAL+ :] ) ) and
A11: ( not b in REAL+ or not a in [:{0 },REAL+ :] ) and
A12: ( not a in REAL+ or not b in [:{0 },REAL+ :] ) ; :: thesis: a = b

( a = -infty or b = +infty ) by A1, A10, A11, Def5;
hence a = b by A2, A10, A12, Def5, Lm6; :: thesis: verum

end;

end;