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:1; :: thesis: verum

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:1; :: thesis: verum