:: deftheorem Def30 defines LTLNodes MODELC_3:def 30 :
for v being LTL-formula
for b₂ being non empty set holds
( b₂ = LTLNodes v iff for x being object holds
( x in b₂ iff ex N being strict LTLnode over v st x = N ) );