let H be CTL-formula; :: thesis: ( H is ExistUntill implies H = (the_left_argument_of H) EU (the_right_argument_of H) )
assume A1: H is ExistUntill ; :: thesis: H = (the_left_argument_of H) EU (the_right_argument_of H)
then H . 1 = 4 by Lm7;
then A2: not H is conjunctive by Lm4;
then ex H1 being CTL-formula st H = H1 EU (the_right_argument_of H) by A1, Def23;
hence H = (the_left_argument_of H) EU (the_right_argument_of H) by A1, A2, Def22; :: thesis: verum