[.r,s.[ is bounded_above

proof

take s ; :: according to XXREAL_2:def 10 :: thesis: s is UpperBound of [.r,s.[
let x be ExtReal; :: 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:3; :: thesis: verum

end;

hence [.r,s.[ is real-bounded ; :: thesis: verum