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 a', b' being Element of REAL+ st
( a = a' & b = b' & a' <=' b' ) & ex b'', a'' being Element of REAL+ st
( b = b'' & a = a'' & b'' <=' a'' ) ) 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 a', b' being Element of REAL+ such that
A6: ( a = [0 ,a'] & b = [0 ,b'] ) and
A7: b' <=' a' by A1, A5, Def5;
consider b'', a'' being Element of REAL+ such that
A8: ( b = [0 ,b''] & a = [0 ,a''] ) and
A9: a'' <=' b'' by A2, A5, Def5;
( a' = a'' & b' = b'' ) 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;