theorem :: MODELC_3:2

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 disjunctive or H is Until or H is Release ) holds
( w |= * N iff ( w |= * (SuccNode1 (H,N)) or w |= * (SuccNode2 (H,N)) ) ) by Lm18, Lm19, Lm20;