theorem Th10: :: MODELC_3:10

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