thus ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st
( p = x & q = y & p <= q ) ) ) ; :: thesis:
thus ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) :: thesis:

proof

assume A1: ( not x in REAL or not y in REAL ) ; :: thesis:

per cases by A1;

suppose A2: not x in REAL ; :: thesis:

thus ( not x <= y or x = -infty or y = +infty ) :: thesis:

proof

assume A3: x <= y ; :: thesis:
assume x <> -infty ; :: thesis:
then x = +infty by A2, XXREAL_0:14;
hence y = +infty by A3, XXREAL_0:4; :: thesis:

end;

thus ( ( x = -infty or y = +infty ) implies x <= y ) by XXREAL_0:3, XXREAL_0:5; :: thesis:

end;

suppose A4: not y in REAL ; :: thesis:

thus ( not x <= y or x = -infty or y = +infty ) :: thesis:

proof

assume A5: x <= y ; :: thesis:
assume A6: x <> -infty ; :: thesis:
assume y <> +infty ; :: thesis:
then y = -infty by A4, XXREAL_0:14;
hence contradiction by A5, A6, XXREAL_0:6; :: thesis:

end;

thus ( ( x = -infty or y = +infty ) implies x <= y ) by XXREAL_0:3, XXREAL_0:5; :: thesis:

end;

end;

end;