let x be ExtReal; :: thesis: x is UpperBound of {}
let y be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( y in {} implies y <= x )
thus ( y in {} implies y <= x ) ; :: thesis: verum