theorem Th14: :: MODELC_3:14
for F, H being LTL-formula
for W being Subset of (Subformulae H) st W = {F} holds
len W = len F