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

inf (INF F) is LowerBound of S

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

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

for x being ExtReal st x in S holds

inf (INF F) <= x

inf (INF F) is LowerBound of S

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

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

for x being ExtReal st x in S holds

inf (INF F) <= x

proof

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

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

then consider Z being set such that

A2: x in Z and

A3: Z in F by A1, TARSKI:def 4;

reconsider Z = Z as non empty ext-real-membered set by A2, A3;

set a = inf Z;

( inf Z is LowerBound of Z & inf Z in INF F ) by A3, Def4, XXREAL_2:def 4;

hence inf (INF F) <= x by A2, XXREAL_2:62, XXREAL_2:def 2; :: thesis: verum

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

then consider Z being set such that

A2: x in Z and

A3: Z in F by A1, TARSKI:def 4;

reconsider Z = Z as non empty ext-real-membered set by A2, A3;

set a = inf Z;

( inf Z is LowerBound of Z & inf Z in INF F ) by A3, Def4, XXREAL_2:def 4;

hence inf (INF F) <= x by A2, XXREAL_2:62, XXREAL_2:def 2; :: thesis: verum