set Old = the LTLold of N \/ {H};
set NewA = the LTLnew of N \ {H};
set NewB = (LTLNew1 H) \ the LTLold of N;
set NewC = (the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N);
set NextD = the LTLnext of N \/ (LTLNext H);
{H} c= Subformulae v by A1, ZFMISC_1:37;
then reconsider Old = the LTLold of N \/ {H} as Subset of (Subformulae v) by XBOOLE_1:8;
consider F being LTL-formula such that
A9: H = F and
A10: F is_subformula_of v by A1, MODELC_2:def 24;
A11: Subformulae H c= Subformulae v by A9, A10, MODELC_2:46;
then (LTLNew1 H) \ the LTLold of N c= Subformulae v by XBOOLE_1:1;
then reconsider NewC = (the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) as Subset of (Subformulae v) by XBOOLE_1:8;
LTLNext H c= Subformulae v by A11, XBOOLE_1:1;
then reconsider NextD = the LTLnext of N \/ (LTLNext H) as Subset of (Subformulae v) by XBOOLE_1:8;
set IT = LTLnode(# Old,NewC,NextD #);
take LTLnode(# Old,NewC,NextD #) ; :: thesis: ( the LTLold of LTLnode(# Old,NewC,NextD #) = the LTLold of N \/ {H} & the LTLnew of LTLnode(# Old,NewC,NextD #) = (the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) & the LTLnext of LTLnode(# Old,NewC,NextD #) = the LTLnext of N \/ (LTLNext H) )
thus ( the LTLold of LTLnode(# Old,NewC,NextD #) = the LTLold of N \/ {H} & the LTLnew of LTLnode(# Old,NewC,NextD #) = (the LTLnew of N \ {H}) \/ ((LTLNew1 H) \ the LTLold of N) & the LTLnext of LTLnode(# Old,NewC,NextD #) = the LTLnext of N \/ (LTLNext H) ) ; :: thesis: verum