reconsider A = {0} as Subset of REAL ;
take A ; :: thesis: ( not A is empty & A is bounded_above & A is bounded_below )
thus not A is empty ; :: thesis: ( A is bounded_above & A is bounded_below )
thus A is bounded_above ; :: thesis: A is bounded_below
take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of A
let t be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not t in A or 0 <= t )
assume t in A ; :: thesis: 0 <= t
hence 0 <= t ; :: thesis: verum