theorem Th5: :: MODELC_3:5

for L being FinSequence
for F, H being LTL-formula
for W being Subset of (Subformulae H) st not F in W holds
len (L,(W \ {F})) = len (L,W)