theorem Th1: :: MODELC_1:1

for a being set holds
( a is CTL-formula iff a in CTL_WFF )