let x be ext-real number ; :: 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 set such that
A7: z in {0 } and
A8: x9 in REAL+ and
A9: x = [z,x9] by A5, ZFMISC_1:103;
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;