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: ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) )
thus ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) :: thesis: verum

proof

assume A1: ( not x in REAL or not y in REAL ) ; :: thesis: ( x <= y iff ( x = -infty or y = +infty ) )

per cases ( not x in REAL or not y in REAL ) by A1;

suppose A2: not x in REAL ; :: thesis: ( x <= y iff ( x = -infty or y = +infty ) )

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

proof

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

end;

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

end;

suppose A4: not y in REAL ; :: thesis: ( x <= y iff ( x = -infty or y = +infty ) )

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

proof

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

end;

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

end;

end;

end;