let A be Subset of REAL; :: thesis: for G being sequence of (bool REAL) st A c= union (rng G) & ( for n being Element of NAT holds G . n is open_interval ) holds
G is Open_Interval_Covering of A
let G be sequence of (bool REAL); :: thesis: ( A c= union (rng G) & ( for n being Element of NAT holds G . n is open_interval ) implies G is Open_Interval_Covering of A )
assume that
A1: A c= union (rng G) and
A2: for n being Element of NAT holds G . n is open_interval ; :: thesis: G is Open_Interval_Covering of A
now :: thesis: for n being Element of NAT holds G . n is Interval
let n be Element of NAT ; :: thesis: G . n is Interval
G . n is open_interval by A2;
hence G . n is Interval ; :: thesis: verum
end;
then G is Interval_Covering of A by A1, MEASURE7:def 2;
hence G is Open_Interval_Covering of A by A2, Def5; :: thesis: verum