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

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