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