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

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

hence inf {x} = x by A1, Def4; :: thesis: verum

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

proof

x is LowerBound of {x}
by Th2;
let z be LowerBound of {x}; :: thesis: z <= x

x in {x} by TARSKI:def 1;

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

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

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

hence inf {x} = x by A1, Def4; :: thesis: verum