:: deftheorem defines CastLTL MODELC_3:def 21 :
for v being LTL-formula
for W being Subset of (Subformulae v) holds CastLTL W = W;