theorem :: MODELC_3:1

for H, v being LTL-formula
for N being strict LTLnode over v
for w being Element of Inf_seq AtomicFamily st H in the LTLnew of N & ( H is atomic or H is negative or H is conjunctive or H is next ) holds
( w |= * N iff w |= * (SuccNode1 (H,N)) ) by Lm16, Lm17;