let F, v be LTL-formula; :: thesis: for N2, N1 being strict LTLnode of v st N2 is_succ_of N1,F holds
F in the LTLold of N2
let N2, N1 be strict LTLnode of v; :: thesis: ( N2 is_succ_of N1,F implies F in the LTLold of N2 )
assume A1: N2 is_succ_of N1,F ; :: thesis: F in the LTLold of N2

now

per cases ( ( F in the LTLnew of N1 & N2 = SuccNode1 F,N1 ) or ( F in the LTLnew of N1 & ( F is disjunctive or F is Until or F is Release ) & N2 = SuccNode2 F,N1 ) ) by A1, DefSucc01;

suppose ( F in the LTLnew of N1 & N2 = SuccNode1 F,N1 ) ; :: thesis: F in the LTLold of N2

then the LTLold of N2 = the LTLold of N1 \/ {F} by Def206;
then B1: {F} c= the LTLold of N2 by XBOOLE_1:7;
F in {F} by TARSKI:def 1;
hence F in the LTLold of N2 by B1; :: thesis: verum

end;

suppose ( F in the LTLnew of N1 & ( F is disjunctive or F is Until or F is Release ) & N2 = SuccNode2 F,N1 ) ; :: thesis: F in the LTLold of N2

then the LTLold of N2 = the LTLold of N1 \/ {F} by Def207;
then B2: {F} c= the LTLold of N2 by XBOOLE_1:7;
F in {F} by TARSKI:def 1;
hence F in the LTLold of N2 by B2; :: thesis: verum

end;

end;

end;

hence F in the LTLold of N2 ; :: thesis: verum