:: deftheorem defines Seed MODELC_3:def 14 :
for v being LTL-formula holds Seed v = {v};