let A, B be Subset of REAL; :: thesis: for F being Interval_Covering of A st B c= A holds
F is Interval_Covering of B
let F be Interval_Covering of A; :: thesis: ( B c= A implies F is Interval_Covering of B )
assume A1: B c= A ; :: thesis: F is Interval_Covering of B
A2: ( A c= union (rng F) & ( for n being Element of NAT holds F . n is Interval ) ) by MEASURE7:def 2;
then B c= union (rng F) by A1;
hence F is Interval_Covering of B by A2, MEASURE7:def 2; :: thesis: verum