let x be ext-real number ; :: thesis: ( ( x in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( x = x' & x = y' & x' <=' y' ) ) & ( x in [:{0 },REAL+ :] & x in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( x = [0 ,x'] & x = [0 ,y'] & y' <=' x' ) ) & ( ( 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 x', y' being Element of REAL+ holds
( not x = x' or not x = y' or not x' <=' y' ) ) ) or ( x in [:{0 },REAL+ :] & x in [:{0 },REAL+ :] & ( for x', y' being Element of REAL+ holds
( not x = [0 ,x'] or not x = [0 ,y'] or not y' <=' x' ) ) ) 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 x', y' being Element of REAL+ holds
( not x = x' or not x = y' or not x' <=' y' ) ) ) or ( x in [:{0 },REAL+ :] & ( for x', y' being Element of REAL+ holds
( not x = [0 ,x'] or not x = [0 ,y'] or not y' <=' x' ) ) ) 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 x', y' being Element of REAL+ holds
( not x = x' or not x = y' or not x' <=' y' ) ; :: thesis: contradiction

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

end;

suppose that A5: x in [:{0 },REAL+ :] and
A6: for x', y' being Element of REAL+ holds
( not x = [0 ,x'] or not x = [0 ,y'] or not y' <=' x' ) ; :: thesis: contradiction

consider z, x' being set such that
A7: z in {0 } and
A8: x' in REAL+ and
A9: x = [z,x'] by A5, ZFMISC_1:103;
reconsider x' = x' as Element of REAL+ by A8;
x = [0 ,x'] by A7, A9, TARSKI:def 1;
then not x' <=' x' 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;