theorem Th16: :: MODELC_3:16

for H being LTL-formula
for W being Subset of (Subformulae H) st len W < 1 holds
W = {} H