theorem Th2: :: MODELC_2:2

for H being LTL-formula holds
( H is atomic or H is negative or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release )