A1: [.r,s.[ is bounded_below

proof

take r ; :: according to SEQ_4:def 2 :: thesis: for b₁ being set holds
( not b₁ in [.r,s.[ or r <= b₁ )
thus for b₁ being set holds
( not b₁ in [.r,s.[ or r <= b₁ ) by XXREAL_1:3; :: thesis: verum

end;

[.r,s.[ is bounded_above

proof

take s ; :: according to SEQ_4:def 1 :: thesis: for b₁ being set holds
( not b₁ in [.r,s.[ or b₁ <= s )
thus for b₁ being set holds
( not b₁ in [.r,s.[ or b₁ <= s ) by XXREAL_1:3; :: thesis: verum

end;

hence for b₁ being Subset of REAL st b₁ = [.r,s.[ holds
b₁ is bounded by A1; :: thesis: verum