let x be ExtReal; :: thesis: sup {x} = x

A1: for z being UpperBound of {x} holds x <= z

hence sup {x} = x by A1, Def3; :: thesis: verum

A1: for z being UpperBound of {x} holds x <= z

proof

x is UpperBound of {x}
by Th1;
let z be UpperBound of {x}; :: thesis: x <= z

x in {x} by TARSKI:def 1;

hence x <= z by Def1; :: thesis: verum

end;x in {x} by TARSKI:def 1;

hence x <= z by Def1; :: thesis: verum

hence sup {x} = x by A1, Def3; :: thesis: verum