A1: [.r1,r2.] is bounded_below

proof

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

end;

[.r1,r2.] is bounded_above

proof

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

end;

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