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

inf S = inf (INF F)

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

set a = inf S;

set b = inf (INF F);

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

then inf S is LowerBound of INF F by Th7;

then A2: inf S <= inf (INF F) by XXREAL_2:def 4;

inf (INF F) is LowerBound of S by A1, Th8;

then inf (INF F) <= inf S by XXREAL_2:def 4;

hence inf S = inf (INF F) by A2, XXREAL_0:1; :: thesis: verum

inf S = inf (INF F)

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

set a = inf S;

set b = inf (INF F);

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

then inf S is LowerBound of INF F by Th7;

then A2: inf S <= inf (INF F) by XXREAL_2:def 4;

inf (INF F) is LowerBound of S by A1, Th8;

then inf (INF F) <= inf S by XXREAL_2:def 4;

hence inf S = inf (INF F) by A2, XXREAL_0:1; :: thesis: verum