set S1 = the LTLold of N;
set S2 = the LTLnew of N;
set S3 = CastLTL the LTLnext of N;
A1: the LTLold of N is Subset of LTL_WFF by MODELC_2:47;
the LTLnew of N is Subset of LTL_WFF by MODELC_2:47;
then A2: the LTLold of N \/ the LTLnew of N c= LTL_WFF by A1, XBOOLE_1:8;
reconsider S3 = CastLTL the LTLnext of N as Subset of LTL_WFF ;
thus (the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N)) is Subset of LTL_WFF by A2, XBOOLE_1:8; :: thesis: verum