:: deftheorem Def25 defines CastLTL MODELC_2:def 25 :
for x being object holds
( ( x in LTL_WFF implies CastLTL x = x ) & ( not x in LTL_WFF implies CastLTL x = atom. 0 ) );