H is Element of CTL_WFF by Def13;
then 'not' H is Element of CTL_WFF by Def12;
hence 'not' H is CTL-formula-like ; :: thesis: verum