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

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