let x, y be ExtReal; :: thesis: ( y is UpperBound of {x} iff x <= y )

x in {x} by TARSKI:def 1;

hence ( y is UpperBound of {x} implies x <= y ) by Def1; :: thesis: ( x <= y implies y is UpperBound of {x} )

assume A1: x <= y ; :: thesis: y is UpperBound of {x}

let z be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( z in {x} implies z <= y )

assume z in {x} ; :: thesis: z <= y

hence z <= y by A1, TARSKI:def 1; :: thesis: verum

x in {x} by TARSKI:def 1;

hence ( y is UpperBound of {x} implies x <= y ) by Def1; :: thesis: ( x <= y implies y is UpperBound of {x} )

assume A1: x <= y ; :: thesis: y is UpperBound of {x}

let z be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( z in {x} implies z <= y )

assume z in {x} ; :: thesis: z <= y

hence z <= y by A1, TARSKI:def 1; :: thesis: verum