set S2 = the LTLnew of N;
set S1 = the LTLold of N;
( the LTLold of N is Subset of LTL_WFF & the LTLnew of N is Subset of LTL_WFF ) by MODELC_2:47;
then the LTLold of N \/ the LTLnew of N c= LTL_WFF by XBOOLE_1:8;
hence ( the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N)) is Subset of LTL_WFF by XBOOLE_1:8; :: thesis: verum