let F be sequence of (bool REAL); :: thesis: for G being sequence of (Funcs (NAT,(bool REAL))) st ( for n being Element of NAT holds G . n is Open_Interval_Covering of F . n ) holds
G is Open_Interval_Covering of F
let G be sequence of (Funcs (NAT,(bool REAL))); :: thesis: ( ( for n being Element of NAT holds G . n is Open_Interval_Covering of F . n ) implies G is Open_Interval_Covering of F )
assume A1: for n being Element of NAT holds G . n is Open_Interval_Covering of F . n ; :: thesis: G is Open_Interval_Covering of F
then for n being Element of NAT holds G . n is Interval_Covering of F . n ;
then G is Interval_Covering of F by MEASURE7:def 3;
hence G is Open_Interval_Covering of F by A1, Def6; :: thesis: verum