:: deftheorem Def10 defines LTL-formula-like MODELC_2:def 10 :
for IT being FinSequence of NAT holds
( IT is LTL-formula-like iff IT is Element of LTL_WFF );