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 & x in 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 or not x in ) & not ( x in REAL+ & x in ) & 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 & x in & ( 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 or not x in ) & not ( x in REAL+ & x in ) & not x = -infty & not x = +infty ) ) ; :: thesis: contradiction
x in ExtREAL by Def1;
then A2: ( x in () \ or x in ) 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 & ( 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 & not ( x in REAL+ & x in ) & 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 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 and
A8: x9 in REAL+ and
A9: x = [z,x9] by ;
reconsider x9 = x9 as Element of REAL+ by A8;
x = [0,x9] by ;
then not x9 <=' x9 by A6;
hence contradiction ; :: thesis: verum
end;
suppose ( not x in REAL+ & not x in & not ( x in REAL+ & x in ) & not x = -infty & not x = +infty ) ; :: thesis: contradiction
end;
end;