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