:: deftheorem defines FinalNode MODELC_3:def 15 :
for v being LTL-formula holds FinalNode v = LTLnode(# ({} v),({} v),({} v) #);