let x, y be ext-real number ; :: thesis: ( x <= y implies y is UpperBound of {x,y} )
assume Z: x <= y ; :: thesis: y is UpperBound of {x,y}
let z be ext-real number ; :: 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 Z, TARSKI:def 2; :: thesis: verum