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 A2:
sup A <> +infty
; :: thesis: A is bounded_above assume A1:
A is bounded_above
; :: thesis: sup A <> +infty

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

end;

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;-infty is UpperBound of A by A3, Def3;

hence 0 is UpperBound of A by Th71; :: thesis: verum

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;take r ; :: according to XXREAL_2:def 10 :: thesis: r is UpperBound of A

thus r is UpperBound of A by Def3; :: thesis: verum