set x = the Element of CTL_WFF ;
reconsider x = the Element of CTL_WFF as FinSequence of NAT by Def12;
take x ; :: thesis: x is CTL-formula-like
thus x is Element of CTL_WFF ; :: according to MODELC_1:def 13 :: thesis: verum