let x, y be ExtReal; :: thesis: for A being ext-real-membered set st x <= y & x is UpperBound of A holds
y is UpperBound of A
let A be ext-real-membered set ; :: thesis: ( x <= y & x is UpperBound of A implies y is UpperBound of A )
assume that
A1: x <= y and
A2: x is UpperBound of A ; :: thesis: y is UpperBound of A
let z be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( z in A implies z <= y )
assume z in A ; :: thesis: z <= y
then z <= x by A2, Def1;
hence z <= y by A1, XXREAL_0:2; :: thesis: verum