theorem Th6: :: MODELC_3:6

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