theorem :: MODELC_2:47

for a being set
for H being LTL-formula st a is Subset of (Subformulae H) holds
a is Subset of LTL_WFF