].r,s.] is bounded_below
proof
take r ; :: according to XXREAL_2:def 9 :: thesis: r is LowerBound of ].r,s.]
let x be ExtReal; :: 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 ].r,s.] is real-bounded ; :: thesis: verum