let a be set ; :: thesis: ( a is CTL-formula iff a in CTL_WFF )
thus ( a is CTL-formula implies a in CTL_WFF ) :: thesis: ( a in CTL_WFF implies a is CTL-formula )

proof

assume a is CTL-formula ; :: thesis: a in CTL_WFF
then a is Element of CTL_WFF by Def13;
hence a in CTL_WFF ; :: thesis: verum

end;

assume a in CTL_WFF ; :: thesis: a is CTL-formula
hence a is CTL-formula by Def12, Def13; :: thesis: verum