let F be bool_DOMAIN of ExtREAL; :: thesis: for S being non empty ext-real-membered set st S = union F holds

inf S is LowerBound of INF F

let S be non empty ext-real-membered set ; :: thesis: ( S = union F implies inf S is LowerBound of INF F )

assume A1: S = union F ; :: thesis: inf S is LowerBound of INF F

for x being ExtReal st x in INF F holds

inf S <= x

inf S is LowerBound of INF F

let S be non empty ext-real-membered set ; :: thesis: ( S = union F implies inf S is LowerBound of INF F )

assume A1: S = union F ; :: thesis: inf S is LowerBound of INF F

for x being ExtReal st x in INF F holds

inf S <= x

proof

hence
inf S is LowerBound of INF F
by XXREAL_2:def 2; :: thesis: verum
let x be ExtReal; :: thesis: ( x in INF F implies inf S <= x )

assume x in INF F ; :: thesis: inf S <= x

then consider A being non empty ext-real-membered set such that

A2: A in F and

A3: x = inf A by Def4;

A c= S by A1, A2, TARSKI:def 4;

hence inf S <= x by A3, XXREAL_2:60; :: thesis: verum

end;assume x in INF F ; :: thesis: inf S <= x

then consider A being non empty ext-real-membered set such that

A2: A in F and

A3: x = inf A by Def4;

A c= S by A1, A2, TARSKI:def 4;

hence inf S <= x by A3, XXREAL_2:60; :: thesis: verum