let A, B be Subset of REAL; :: thesis: for F being Open_Interval_Covering of A st B c= A holds
F is Open_Interval_Covering of B
let F be Open_Interval_Covering of A; :: thesis: ( B c= A implies F is Open_Interval_Covering of B )
assume B c= A ; :: thesis: F is Open_Interval_Covering of B
then A1: F is Interval_Covering of B by Th37;
for n being Element of NAT holds F . n is open_interval ;
hence F is Open_Interval_Covering of B by A1, Def5; :: thesis: verum