set NextD = the LTLnext of N;
set NewB = (LTLNew2 H) \ the LTLold of N;
set NewA = the LTLnew of N \ {H};
set Old = the LTLold of N \/ {H};
set NewC = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N);
{H} c= Subformulae v
by A1, ZFMISC_1:31;
then reconsider Old = the LTLold of N \/ {H} as Subset of (Subformulae v) by XBOOLE_1:8;
ex F being LTL-formula st
( H = F & F is_subformula_of v )
by A1, MODELC_2:def 24;
then
Subformulae H c= Subformulae v
by MODELC_2:46;
then
(LTLNew2 H) \ the LTLold of N c= Subformulae v
;
then reconsider NewC = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) as Subset of (Subformulae v) by XBOOLE_1:8;
set IT = LTLnode(# Old,NewC, the LTLnext of N #);
take
LTLnode(# Old,NewC, the LTLnext of N #)
; ( the LTLold of LTLnode(# Old,NewC, the LTLnext of N #) = the LTLold of N \/ {H} & the LTLnew of LTLnode(# Old,NewC, the LTLnext of N #) = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) & the LTLnext of LTLnode(# Old,NewC, the LTLnext of N #) = the LTLnext of N )
thus
( the LTLold of LTLnode(# Old,NewC, the LTLnext of N #) = the LTLold of N \/ {H} & the LTLnew of LTLnode(# Old,NewC, the LTLnext of N #) = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) & the LTLnext of LTLnode(# Old,NewC, the LTLnext of N #) = the LTLnext of N )
; verum