A1: [.r1,r2.] is bounded_above

proof

take r2 ; :: according to XXREAL_2:def 10 :: thesis: r2 is UpperBound of [.r1,r2.]
let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not x in [.r1,r2.] or x <= r2 )
thus ( not x in [.r1,r2.] or x <= r2 ) by XXREAL_1:1; :: thesis: verum

end;

[.r1,r2.] is bounded_below

proof

take r1 ; :: according to XXREAL_2:def 9 :: thesis: r1 is LowerBound of [.r1,r2.]
let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not x in [.r1,r2.] or r1 <= x )
thus ( not x in [.r1,r2.] or r1 <= x ) by XXREAL_1:1; :: thesis: verum

end;

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