let X be ext-real-membered non empty set ; :: thesis: for x being LowerBound of X st x in X holds
x = inf X
let x be LowerBound of X; :: thesis: ( x in X implies x = inf X )
assume x in X ; :: thesis: x = inf X
then for y being LowerBound of X holds y <= x by Def2;
hence x = inf X by Def4; :: thesis: verum