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

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+:] ) ) )
;

end;

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;( 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

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;hence a = b by A1, A3, Def5, Lm4, Lm5; :: thesis: verum

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;hence a = b by A2, A4, Def5, Lm4, Lm5; :: thesis: verum

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;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

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

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;hence a = b by A2, A10, A12, Def5, Lm7; :: thesis: verum