let x be ext-real number ; :: thesis: inf {x} = x
A: x is LowerBound of {x} by Th2;
for z being LowerBound of {x} holds z <= x

proof

let z be LowerBound of {x}; :: thesis: z <= x
x in {x} by TARSKI:def 1;
hence z <= x by Def2; :: thesis: verum

end;

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