:: deftheorem Def16 defines CastNode MODELC_3:def 16 :
for x being object
for v being LTL-formula holds
( ( x is strict LTLnode over v implies CastNode (x,v) = x ) & ( x is not strict LTLnode over v implies CastNode (x,v) = LTLnode(# ({} v),({} v),({} v) #) ) );