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

now

per cases ( N2 is_succ1_of N1 or N2 is_succ2_of N1 ) by A1, Def210;

suppose N2 is_succ1_of N1 ; :: thesis: N2 is_succ_of N1,F

then consider H being LTL-formula such that
B1: H in the LTLnew of N1 and
B2: N2 = SuccNode1 H,N1 by Def208;
the LTLold of N2 = the LTLold of N1 \/ {H} by Def206, B1, B2;
then ( F in the LTLold of N1 or F in {H} ) by A3, XBOOLE_0:def 3;
then F = H by A2, TARSKI:def 1;
hence N2 is_succ_of N1,F by DefSucc01, B1, B2; :: thesis: verum

end;

suppose N2 is_succ2_of N1 ; :: thesis: N2 is_succ_of N1,F

then consider H being LTL-formula such that
B1: H in the LTLnew of N1 and
B2: ( H is disjunctive or H is Until or H is Release ) and
B3: N2 = SuccNode2 H,N1 by Def209;
the LTLold of N2 = the LTLold of N1 \/ {H} by Def207, B1, B2, B3;
then ( F in the LTLold of N1 or F in {H} ) by A3, XBOOLE_0:def 3;
then F = H by A2, TARSKI:def 1;
hence N2 is_succ_of N1,F by DefSucc01, B1, B2, B3; :: thesis: verum

end;

end;

end;

hence N2 is_succ_of N1,F ; :: thesis: verum