EX H is CTL-formula-like
proof
H is Element of CTL_WFF by Def13;
hence EX H is Element of CTL_WFF by Def12; :: according to MODELC_1:def 13 :: thesis: verum
end;
hence EX H is CTL-formula-like ; :: thesis: verum