let x, y be ExtReal; :: thesis: ( ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds

( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds

( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) implies ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) )

assume A10: ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds

( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds

( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

x in ExtREAL by Def1;

then A11: ( x in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or x in {+infty,-infty} ) by XBOOLE_0:def 3;

y in ExtREAL by Def1;

then A12: ( y in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or y in {+infty,-infty} ) by XBOOLE_0:def 3;

( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds

( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) implies ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) )

assume A10: ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds

( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds

( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

x in ExtREAL by Def1;

then A11: ( x in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or x in {+infty,-infty} ) by XBOOLE_0:def 3;

y in ExtREAL by Def1;

then A12: ( y in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or y in {+infty,-infty} ) by XBOOLE_0:def 3;

per cases
( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds

( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds

( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) by A10;

end;

( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds

( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) by A10;

suppose that A13:
( x in REAL+ & y in REAL+ )
and

A14: for x9, y9 being Element of REAL+ holds

( not x = x9 or not y = y9 or not x9 <=' y9 ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) by A13, ARYTM_0:5, XBOOLE_0:3; :: thesis: verum

end;

A14: for x9, y9 being Element of REAL+ holds

( not x = x9 or not y = y9 or not x9 <=' y9 ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

hereby :: thesis: ( ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

thus
( ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

assume
( y in REAL+ & x in REAL+ )
; :: thesis: ex y9, x9 being Element of REAL+ st

( y = y9 & x = x9 & y9 <=' x9 )

then reconsider x9 = x, y9 = y as Element of REAL+ ;

take y9 = y9; :: thesis: ex x9 being Element of REAL+ st

( y = y9 & x = x9 & y9 <=' x9 )

take x9 = x9; :: thesis: ( y = y9 & x = x9 & y9 <=' x9 )

thus ( y = y9 & x = x9 ) ; :: thesis: y9 <=' x9

thus y9 <=' x9 by A14; :: thesis: verum

end;( y = y9 & x = x9 & y9 <=' x9 )

then reconsider x9 = x, y9 = y as Element of REAL+ ;

take y9 = y9; :: thesis: ex x9 being Element of REAL+ st

( y = y9 & x = x9 & y9 <=' x9 )

take x9 = x9; :: thesis: ( y = y9 & x = x9 & y9 <=' x9 )

thus ( y = y9 & x = x9 ) ; :: thesis: y9 <=' x9

thus y9 <=' x9 by A14; :: thesis: verum

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) by A13, ARYTM_0:5, XBOOLE_0:3; :: thesis: verum

suppose that A15:
( x in [:{0},REAL+:] & y in [:{0},REAL+:] )
and

A16: for x9, y9 being Element of REAL+ holds

( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) by A15, ARYTM_0:5, XBOOLE_0:3; :: thesis: verum

end;

A16: for x9, y9 being Element of REAL+ holds

( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

now :: thesis: ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex y9, x9 being Element of REAL+ st

( y = [0,y9] & x = [0,x9] & x9 <=' y9 ) )

hence
( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st ( y = [0,y9] & x = [0,x9] & x9 <=' y9 ) )

assume
y in [:{0},REAL+:]
; :: thesis: ( x in [:{0},REAL+:] implies ex y9, x9 being Element of REAL+ st

( y = [0,y9] & x = [0,x9] & x9 <=' y9 ) )

then consider z, y9 being object such that

A17: z in {0} and

A18: y9 in REAL+ and

A19: y = [z,y9] by ZFMISC_1:84;

A20: z = 0 by A17, TARSKI:def 1;

assume x in [:{0},REAL+:] ; :: thesis: ex y9, x9 being Element of REAL+ st

( y = [0,y9] & x = [0,x9] & x9 <=' y9 )

then consider z, x9 being object such that

A21: z in {0} and

A22: x9 in REAL+ and

A23: x = [z,x9] by ZFMISC_1:84;

reconsider x9 = x9, y9 = y9 as Element of REAL+ by A18, A22;

take y9 = y9; :: thesis: ex x9 being Element of REAL+ st

( y = [0,y9] & x = [0,x9] & x9 <=' y9 )

take x9 = x9; :: thesis: ( y = [0,y9] & x = [0,x9] & x9 <=' y9 )

thus ( y = [0,y9] & x = [0,x9] ) by A17, A19, A21, A23, TARSKI:def 1; :: thesis: x9 <=' y9

z = 0 by A21, TARSKI:def 1;

hence x9 <=' y9 by A16, A19, A20, A23; :: thesis: verum

end;( y = [0,y9] & x = [0,x9] & x9 <=' y9 ) )

then consider z, y9 being object such that

A17: z in {0} and

A18: y9 in REAL+ and

A19: y = [z,y9] by ZFMISC_1:84;

A20: z = 0 by A17, TARSKI:def 1;

assume x in [:{0},REAL+:] ; :: thesis: ex y9, x9 being Element of REAL+ st

( y = [0,y9] & x = [0,x9] & x9 <=' y9 )

then consider z, x9 being object such that

A21: z in {0} and

A22: x9 in REAL+ and

A23: x = [z,x9] by ZFMISC_1:84;

reconsider x9 = x9, y9 = y9 as Element of REAL+ by A18, A22;

take y9 = y9; :: thesis: ex x9 being Element of REAL+ st

( y = [0,y9] & x = [0,x9] & x9 <=' y9 )

take x9 = x9; :: thesis: ( y = [0,y9] & x = [0,x9] & x9 <=' y9 )

thus ( y = [0,y9] & x = [0,x9] ) by A17, A19, A21, A23, TARSKI:def 1; :: thesis: x9 <=' y9

z = 0 by A21, TARSKI:def 1;

hence x9 <=' y9 by A16, A19, A20, A23; :: thesis: verum

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) by A15, ARYTM_0:5, XBOOLE_0:3; :: thesis: verum

suppose
( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty )
; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

hence
( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) by A11, A12, TARSKI:def 2, XBOOLE_0:def 3; :: thesis: verum

end;( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st

( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) by A11, A12, TARSKI:def 2, XBOOLE_0:def 3; :: thesis: verum