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 SEQ_4:def 2 :: thesis: for b₁ being set holds
( not b₁ in A or 0 <= b₁ )
let t be real number ; :: thesis: ( not t in A or 0 <= t )
assume t in A ; :: thesis: 0 <= t
hence 0 <= t ; :: thesis: verum