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 ( not H is negative & not H is ExistNext ) by Lm18;
hence H = EG (the_argument_of H) by A1, Def21; :: thesis: verum