theorem :: MODELC_3:43

for v being LTL-formula holds init v is Element of LTLStates v