let x, y be ExtReal; :: thesis: y is UpperBound of ].x,y.[
let z be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( z in ].x,y.[ implies z <= y )
assume z in ].x,y.[ ; :: thesis: z <= y
hence z <= y by XXREAL_1:4; :: thesis: verum