theorem Th1: :: MODELC_2:1

for a being set holds
( a is LTL-formula iff a in LTL_WFF )