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 b1 being Subset of REAL st b1 = [.r1,r2.] holds
b1 is real-bounded by A1; :: thesis: verum