let H be CTL-formula; :: thesis: ( H is ExistGlobal implies H = EG (the_argument_of H) )
assume A1: H is ExistGlobal ; :: thesis: H = EG (the_argument_of H)
then A2: not H is ExistNext by Lm18;
not H is negative by A1, Lm18;
hence H = EG (the_argument_of H) by A1, A2, Def21; :: thesis: verum