let x, y be ExtReal; :: thesis: ( ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in & y in & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in or not y in ) & not ( y in REAL+ & x in ) & not x = -infty & not y = +infty ) ) implies ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in & x in implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in or not x in ) & not ( x in REAL+ & y in ) & not y = -infty implies x = +infty ) ) )

assume A10: ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in & y in & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in or not y in ) & not ( y in REAL+ & x in ) & not x = -infty & not y = +infty ) ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in & x in implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in or not x in ) & not ( x in REAL+ & y in ) & not y = -infty implies x = +infty ) )

x in ExtREAL by Def1;
then A11: ( x in () \ or x in ) by XBOOLE_0:def 3;
y in ExtREAL by Def1;
then A12: ( y in () \ or y in ) by XBOOLE_0:def 3;
per cases ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in & y in & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in or not y in ) & not ( y in REAL+ & x in ) & not x = -infty & not y = +infty ) )
by A10;
suppose that A13: ( x in REAL+ & y in REAL+ ) and
A14: for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in & x in implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in or not x in ) & not ( x in REAL+ & y in ) & not y = -infty implies x = +infty ) )

hereby :: thesis: ( ( y in & x in implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in or not x in ) & not ( x in REAL+ & y in ) & not y = -infty implies x = +infty ) )
assume ( y in REAL+ & x in REAL+ ) ; :: thesis: ex y9, x9 being Element of REAL+ st
( y = y9 & x = x9 & y9 <=' x9 )

then reconsider x9 = x, y9 = y as Element of REAL+ ;
take y9 = y9; :: thesis: ex x9 being Element of REAL+ st
( y = y9 & x = x9 & y9 <=' x9 )

take x9 = x9; :: thesis: ( y = y9 & x = x9 & y9 <=' x9 )
thus ( y = y9 & x = x9 ) ; :: thesis: y9 <=' x9
thus y9 <=' x9 by A14; :: thesis: verum
end;
thus ( ( y in & x in implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in or not x in ) & not ( x in REAL+ & y in ) & not y = -infty implies x = +infty ) ) by ; :: thesis: verum
end;
suppose that A15: ( x in & y in ) and
A16: for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in & x in implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in or not x in ) & not ( x in REAL+ & y in ) & not y = -infty implies x = +infty ) )

now :: thesis: ( y in & x in implies ex y9, x9 being Element of REAL+ st
( y = [0,y9] & x = [0,x9] & x9 <=' y9 ) )
assume y in ; :: thesis: ( x in implies ex y9, x9 being Element of REAL+ st
( y = [0,y9] & x = [0,x9] & x9 <=' y9 ) )

then consider z, y9 being object such that
A17: z in and
A18: y9 in REAL+ and
A19: y = [z,y9] by ZFMISC_1:84;
A20: z = 0 by ;
assume x in ; :: thesis: ex y9, x9 being Element of REAL+ st
( y = [0,y9] & x = [0,x9] & x9 <=' y9 )

then consider z, x9 being object such that
A21: z in and
A22: x9 in REAL+ and
A23: x = [z,x9] by ZFMISC_1:84;
reconsider x9 = x9, y9 = y9 as Element of REAL+ by ;
take y9 = y9; :: thesis: ex x9 being Element of REAL+ st
( y = [0,y9] & x = [0,x9] & x9 <=' y9 )

take x9 = x9; :: thesis: ( y = [0,y9] & x = [0,x9] & x9 <=' y9 )
thus ( y = [0,y9] & x = [0,x9] ) by ; :: thesis: x9 <=' y9
z = 0 by ;
hence x9 <=' y9 by A16, A19, A20, A23; :: thesis: verum
end;
hence ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in & x in implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in or not x in ) & not ( x in REAL+ & y in ) & not y = -infty implies x = +infty ) ) by ; :: thesis: verum
end;
suppose ( ( not x in REAL+ or not y in REAL+ ) & ( not x in or not y in ) & not ( y in REAL+ & x in ) & not x = -infty & not y = +infty ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in & x in implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in or not x in ) & not ( x in REAL+ & y in ) & not y = -infty implies x = +infty ) )

hence ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in & x in implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in or not x in ) & not ( x in REAL+ & y in ) & not y = -infty implies x = +infty ) ) by ; :: thesis: verum
end;
end;