let a, b be ExtReal; :: 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, Lm4, Lm5; :: 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, Lm4, Lm5; :: 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, XTUPLE_0:1;
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, Lm7; :: 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, Lm7; :: thesis: verum

end;

end;