consider x being Element of LTL_WFF ;
reconsider x = x as FinSequence of NAT by Def12;
take x ; :: thesis: x is LTL-formula-like
thus x is Element of LTL_WFF ; :: according to MODELC_2:def 10 :: thesis: verum