A2: ].r,s.] is bounded_above

proof

take s ; :: according to XXREAL_2:def 10 :: thesis: s is UpperBound of ].r,s.]
let x be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( not x in ].r,s.] or x <= s )
thus ( not x in ].r,s.] or x <= s ) by XXREAL_1:2; :: thesis: verum

end;

].r,s.] is bounded_below

proof

take r ; :: according to XXREAL_2:def 9 :: thesis: r is LowerBound of ].r,s.]
let x be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not x in ].r,s.] or r <= x )
thus ( not x in ].r,s.] or r <= x ) by XXREAL_1:2; :: thesis: verum

end;

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