let x, y be real number ; :: thesis: ( x <= y & y <= x implies x = y )
assume that
A1:
x <= y
and
A2:
y <= x
; :: thesis: 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 that A4:
x in REAL+
and A5:
y in REAL+
;
:: thesis: x = yconsider x',
y' being
Element of
REAL+ such that A6:
x = x'
and A7:
y = y'
and A8:
x' <=' y'
by A1, A4, A5, XXREAL_0:def 5;
consider y'',
x'' being
Element of
REAL+ such that A9:
y = y''
and A10:
x = x''
and A11:
y'' <=' x''
by A2, A4, A5, XXREAL_0:def 5;
thus
x = y
by A6, A7, A8, A9, A10, A11, ARYTM_1:4;
:: thesis: verum end; suppose that A14:
x in [:{0 },REAL+ :]
and A15:
y in [:{0 },REAL+ :]
;
:: thesis: x = yconsider x',
y' being
Element of
REAL+ such that A16:
x = [0 ,x']
and A17:
y = [0 ,y']
and A18:
y' <=' x'
by A1, A14, A15, XXREAL_0:def 5;
consider y'',
x'' being
Element of
REAL+ such that A19:
y = [0 ,y'']
and A20:
x = [0 ,x'']
and A21:
x'' <=' y''
by A2, A14, A15, XXREAL_0:def 5;
(
x' = x'' &
y' = y'' )
by A16, A17, A19, A20, ZFMISC_1:33;
hence
x = y
by A18, A19, A20, A21, ARYTM_1:4;
:: thesis: verum end;