:: deftheorem defines InitS_LTL MODELC_3:def 44 :
for v being neg-inner-most LTL-formula holds InitS_LTL v = {(init v)};