let x, y be Real; ( x <= y & y <= x implies x = y )
assume that
A1:
x <= y
and
A2:
y <= x
; x = y
A3:
( x in REAL & y in REAL )
by XREAL_0:def 1;
per cases
( ( x in REAL+ & y in REAL+ ) or ( x in REAL+ & y in [:{0},REAL+:] ) or ( y in REAL+ & x in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] ) )
by A3, NUMBERS:def 1, XBOOLE_0:def 3;
suppose A6:
(
x in [:{0},REAL+:] &
y in [:{0},REAL+:] )
;
x = yconsider x9,
y9 being
Element of
REAL+ such that A7:
(
x = [0,x9] &
y = [0,y9] )
and A8:
y9 <=' x9
by A1, A6, XXREAL_0:def 5;
consider y99,
x99 being
Element of
REAL+ such that A9:
(
y = [0,y99] &
x = [0,x99] )
and A10:
x99 <=' y99
by A2, A6, XXREAL_0:def 5;
(
x9 = x99 &
y9 = y99 )
by A7, A9, XTUPLE_0:1;
hence
x = y
by A8, A9, A10, ARYTM_1:4;
verum end; end;