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;

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;

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

reconsider x9 = x as Element of REAL+ by A3;
not x9 <=' x9 by A4;
hence contradiction ; :: thesis: verum

end;

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

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;

suppose ( not x in REAL+ & not x in [:{0},REAL+:] & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not x = +infty ) ; :: thesis: contradiction

hence contradiction by A2, TARSKI:def 2, XBOOLE_0:def 3; :: thesis: verum

end;

end;