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