A2: G is Element of CTL_WFF by Def13;
H is Element of CTL_WFF by Def13;
then H EU G is Element of CTL_WFF by A2, Def12;
hence H EU G is CTL-formula-like ; :: thesis: verum