theorem Th18: :: MODELC_3:18

for H being LTL-formula
for W, W1, W2 being Subset of (Subformulae H) st W = W1 \/ W2 holds
len W <= (len W1) + (len W2)