let x, y be ext-real number ; :: thesis: ( ( ( x in REAL+ & y in REAL+ & ( for x', y' being Element of REAL+ holds
( not x = x' or not y = y' or not x' <=' y' ) ) ) or ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ( for x', y' being Element of REAL+ holds
( not x = [0 ,x'] or not y = [0 ,y'] or not y' <=' x' ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0 },REAL+ :] or not y in [:{0 },REAL+ :] ) & not ( y in REAL+ & x in [:{0 },REAL+ :] ) & not x = -infty & not y = +infty ) ) implies ( ( y in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( y = x' & x = y' & x' <=' y' ) ) & ( y in [:{0 },REAL+ :] & x in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( y = [0 ,x'] & x = [0 ,y'] & y' <=' x' ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0 },REAL+ :] or not x in [:{0 },REAL+ :] ) & not ( x in REAL+ & y in [:{0 },REAL+ :] ) & not y = -infty implies x = +infty ) ) )
assume A10: ( ( x in REAL+ & y in REAL+ & ( for x', y' being Element of REAL+ holds
( not x = x' or not y = y' or not x' <=' y' ) ) ) or ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ( for x', y' being Element of REAL+ holds
( not x = [0 ,x'] or not y = [0 ,y'] or not y' <=' x' ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0 },REAL+ :] or not y in [:{0 },REAL+ :] ) & not ( y in REAL+ & x in [:{0 },REAL+ :] ) & not x = -infty & not y = +infty ) ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( y = x' & x = y' & x' <=' y' ) ) & ( y in [:{0 },REAL+ :] & x in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( y = [0 ,x'] & x = [0 ,y'] & y' <=' x' ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0 },REAL+ :] or not x in [:{0 },REAL+ :] ) & not ( x in REAL+ & y in [:{0 },REAL+ :] ) & not y = -infty implies x = +infty ) )
( x in ExtREAL & y in ExtREAL ) by Def1;
then A11: ( ( x in (REAL+ \/ [:{0 },REAL+ :]) \ {[0 ,0 ]} or x in {+infty ,-infty } ) & ( y in (REAL+ \/ [:{0 },REAL+ :]) \ {[0 ,0 ]} or y in {+infty ,-infty } ) ) by XBOOLE_0:def 3;

per cases ( ( x in REAL+ & y in REAL+ & ( for x', y' being Element of REAL+ holds
( not x = x' or not y = y' or not x' <=' y' ) ) ) or ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] & ( for x', y' being Element of REAL+ holds
( not x = [0 ,x'] or not y = [0 ,y'] or not y' <=' x' ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0 },REAL+ :] or not y in [:{0 },REAL+ :] ) & not ( y in REAL+ & x in [:{0 },REAL+ :] ) & not x = -infty & not y = +infty ) ) by A10;

suppose that A12: ( x in REAL+ & y in REAL+ ) and
A13: for x', y' being Element of REAL+ holds
( not x = x' or not y = y' or not x' <=' y' ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( y = x' & x = y' & x' <=' y' ) ) & ( y in [:{0 },REAL+ :] & x in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( y = [0 ,x'] & x = [0 ,y'] & y' <=' x' ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0 },REAL+ :] or not x in [:{0 },REAL+ :] ) & not ( x in REAL+ & y in [:{0 },REAL+ :] ) & not y = -infty implies x = +infty ) )

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

assume ( y in REAL+ & x in REAL+ ) ; :: thesis: ex y', x' being Element of REAL+ st
( y = y' & x = x' & y' <=' x' )
then reconsider x' = x, y' = y as Element of REAL+ ;
take y' = y'; :: thesis: ex x' being Element of REAL+ st
( y = y' & x = x' & y' <=' x' )
take x' = x'; :: thesis: ( y = y' & x = x' & y' <=' x' )
thus ( y = y' & x = x' ) ; :: thesis: y' <=' x'
thus y' <=' x' by A13; :: thesis: verum

end;

thus ( ( y in [:{0 },REAL+ :] & x in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( y = [0 ,x'] & x = [0 ,y'] & y' <=' x' ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0 },REAL+ :] or not x in [:{0 },REAL+ :] ) & not ( x in REAL+ & y in [:{0 },REAL+ :] ) & not y = -infty implies x = +infty ) ) by A12, ARYTM_0:5, XBOOLE_0:3; :: thesis: verum

end;

suppose that A14: ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] ) and
A15: for x', y' being Element of REAL+ holds
( not x = [0 ,x'] or not y = [0 ,y'] or not y' <=' x' ) ; :: thesis: ( ( y in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( y = x' & x = y' & x' <=' y' ) ) & ( y in [:{0 },REAL+ :] & x in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( y = [0 ,x'] & x = [0 ,y'] & y' <=' x' ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0 },REAL+ :] or not x in [:{0 },REAL+ :] ) & not ( x in REAL+ & y in [:{0 },REAL+ :] ) & not y = -infty implies x = +infty ) )

now

assume y in [:{0 },REAL+ :] ; :: thesis: ( x in [:{0 },REAL+ :] implies ex y', x' being Element of REAL+ st
( y = [0 ,y'] & x = [0 ,x'] & x' <=' y' ) )
then consider z, y' being set such that
A16: z in {0 } and
A17: y' in REAL+ and
A18: y = [z,y'] by ZFMISC_1:103;
A19: z = 0 by A16, TARSKI:def 1;
assume x in [:{0 },REAL+ :] ; :: thesis: ex y', x' being Element of REAL+ st
( y = [0 ,y'] & x = [0 ,x'] & x' <=' y' )
then consider z, x' being set such that
A20: z in {0 } and
A21: x' in REAL+ and
A22: x = [z,x'] by ZFMISC_1:103;
A23: z = 0 by A20, TARSKI:def 1;
reconsider x' = x', y' = y' as Element of REAL+ by A17, A21;
take y' = y'; :: thesis: ex x' being Element of REAL+ st
( y = [0 ,y'] & x = [0 ,x'] & x' <=' y' )
take x' = x'; :: thesis: ( y = [0 ,y'] & x = [0 ,x'] & x' <=' y' )
thus ( y = [0 ,y'] & x = [0 ,x'] ) by A16, A18, A20, A22, TARSKI:def 1; :: thesis: x' <=' y'
thus x' <=' y' by A15, A18, A19, A22, A23; :: thesis: verum

end;

hence ( ( y in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( y = x' & x = y' & x' <=' y' ) ) & ( y in [:{0 },REAL+ :] & x in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( y = [0 ,x'] & x = [0 ,y'] & y' <=' x' ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0 },REAL+ :] or not x in [:{0 },REAL+ :] ) & not ( x in REAL+ & y in [:{0 },REAL+ :] ) & not y = -infty implies x = +infty ) ) by A14, ARYTM_0:5, XBOOLE_0:3; :: thesis: verum

end;

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

hence ( ( y in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( y = x' & x = y' & x' <=' y' ) ) & ( y in [:{0 },REAL+ :] & x in [:{0 },REAL+ :] implies ex x', y' being Element of REAL+ st
( y = [0 ,x'] & x = [0 ,y'] & y' <=' x' ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0 },REAL+ :] or not x in [:{0 },REAL+ :] ) & not ( x in REAL+ & y in [:{0 },REAL+ :] ) & not y = -infty implies x = +infty ) ) by A11, TARSKI:def 2, XBOOLE_0:def 3; :: thesis: verum

end;

end;