theorem Th3: :: MODELC_3:3

for H being LTL-formula ex L being FinSequence st Subformulae H = rng L