:: deftheorem Def13 defines CTL-formula-like MODELC_1:def 13 :
for IT being FinSequence of NAT holds
( IT is CTL-formula-like iff IT is Element of CTL_WFF );