let x be ExtReal; :: thesis: ( ( x in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st

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

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

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

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

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

x in ExtREAL by Def1;

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

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

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

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

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

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

x in ExtREAL by Def1;

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

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

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

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

end;

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

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

suppose that A3:
x in REAL+
and

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

( not x = x9 or not x = y9 or not x9 <=' y9 ) ; :: thesis: contradiction

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

( not x = x9 or not x = y9 or not x9 <=' y9 ) ; :: thesis: contradiction

reconsider x9 = x as Element of REAL+ by A3;

not x9 <=' x9 by A4;

hence contradiction ; :: thesis: verum

end;not x9 <=' x9 by A4;

hence contradiction ; :: thesis: verum

suppose that A5:
x in [:{0},REAL+:]
and

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

( not x = [0,x9] or not x = [0,y9] or not y9 <=' x9 ) ; :: thesis: contradiction

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

( not x = [0,x9] or not x = [0,y9] or not y9 <=' x9 ) ; :: thesis: contradiction

consider z, x9 being object such that

A7: z in {0} and

A8: x9 in REAL+ and

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

reconsider x9 = x9 as Element of REAL+ by A8;

x = [0,x9] by A7, A9, TARSKI:def 1;

then not x9 <=' x9 by A6;

hence contradiction ; :: thesis: verum

end;A7: z in {0} and

A8: x9 in REAL+ and

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

reconsider x9 = x9 as Element of REAL+ by A8;

x = [0,x9] by A7, A9, TARSKI:def 1;

then not x9 <=' x9 by A6;

hence contradiction ; :: thesis: verum