let x, y be ext-real number ; :: thesis:
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:
x in ExtREAL by Def1;
then A11: ( x in (REAL+ \/ [:{0 },REAL+ :]) \ {[0 ,0 ]} or x in {+infty ,-infty } ) by XBOOLE_0:def 3;
y in ExtREAL by Def1;
then A12: ( y in (REAL+ \/ [:{0 },REAL+ :]) \ {[0 ,0 ]} or y in {+infty ,-infty } ) by XBOOLE_0:def 3;

per cases by A10;

suppose that A13: ( x in REAL+ & y in REAL+ ) and
A14: for x', y' being Element of REAL+ holds
( not x = x' or not y = y' or not x' <=' y' ) ; :: thesis:

hereby :: thesis:

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

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 A13, ARYTM_0:5, XBOOLE_0:3; :: thesis:

end;

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

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

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 A15, ARYTM_0:5, XBOOLE_0:3; :: thesis:

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:

end;