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