theorem Th15: :: MODELC_3:15

for H being LTL-formula
for W, W1 being Subset of (Subformulae H) st W c= W1 holds
len W <= len W1