theorem Th11: :: MODELC_3:11

for F, H being LTL-formula
for W, W1 being Subset of (Subformulae H) st not F in W & W1 = W \/ {F} holds
len W1 = (len W) + (len F)