theorem Th17: :: MODELC_3:17

for H being LTL-formula
for W being Subset of (Subformulae H) holds len W >= 0