let A be ext-real-membered set ; :: thesis: ( A is bounded_above iff sup A <> +infty )

hereby :: thesis: ( sup A <> +infty implies A is bounded_above )

assume A1: A is bounded_above ; :: thesis: sup A <> +infty

per cases ( A = {} or A = {-infty} or sup A in REAL ) by A1, Th57;

suppose A = {} ; :: thesis: sup A <> +infty

hence sup A <> +infty by Th39; :: thesis: verum

end;

suppose A = {-infty} ; :: thesis: sup A <> +infty

hence sup A <> +infty by Lm1; :: thesis: verum

end;

suppose sup A in REAL ; :: thesis: sup A <> +infty

hence sup A <> +infty ; :: thesis: verum

end;

end;

end;

assume A2: sup A <> +infty ; :: thesis: A is bounded_above

per cases ( sup A = -infty or sup A in REAL ) by A2, XXREAL_0:14;

suppose A3: sup A = -infty ; :: thesis: A is bounded_above

take 0 ; :: according to XXREAL_2:def 10 :: thesis: 0 is UpperBound of A
-infty is UpperBound of A by A3, Def3;
hence 0 is UpperBound of A by Th71; :: thesis: verum

end;

suppose sup A in REAL ; :: thesis: A is bounded_above

then reconsider r = sup A as Real ;
take r ; :: according to XXREAL_2:def 10 :: thesis: r is UpperBound of A
thus r is UpperBound of A by Def3; :: thesis: verum

end;

end;