let H be CTL-formula; :: thesis: ( ( H is negative or H is ExistNext or H is ExistGlobal ) implies len (the_argument_of H) < len H )
assume A1: ( H is negative or H is ExistNext or H is ExistGlobal ) ; :: thesis: len (the_argument_of H) < len H

per cases ( H is negative or H is ExistNext or H is ExistGlobal ) by A1;

suppose H is negative ; :: thesis: len (the_argument_of H) < len H

then H = 'not' (the_argument_of H) by Def21;
then len H = 1 + (len (the_argument_of H)) by FINSEQ_5:8;
hence len (the_argument_of H) < len H by NAT_1:19; :: thesis: verum

end;

suppose H is ExistNext ; :: thesis: len (the_argument_of H) < len H

then H = EX (the_argument_of H) by Def21;
then len H = 1 + (len (the_argument_of H)) by FINSEQ_5:8;
hence len (the_argument_of H) < len H by NAT_1:19; :: thesis: verum

end;

suppose H is ExistGlobal ; :: thesis: len (the_argument_of H) < len H

then H = EG (the_argument_of H) by Lm19;
then len H = 1 + (len (the_argument_of H)) by FINSEQ_5:8;
hence len (the_argument_of H) < len H by NAT_1:19; :: thesis: verum

end;

end;