let F, v be LTL-formula; :: thesis: for N1, N2 being strict LTLnode over v st N2 is_succ_of N1,F holds
F in the LTLold of N2
let N1, N2 be strict LTLnode over 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 :: thesis: F in the LTLold of N2

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;

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 Def4;
then A2: {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 A2; :: 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 Def5;
then A3: {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 A3; :: thesis: verum

end;

end;

end;

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