let H be LTL-formula; :: thesis: ( ( H is negative or H is next ) implies ( len H = 1 + (len (the_argument_of H)) & len (the_argument_of H) < len H ) )
assume A1: ( H is negative or H is next ) ; :: thesis: ( len H = 1 + (len (the_argument_of H)) & len (the_argument_of H) < len H )

per cases ( H is negative or H is next ) by A1;

suppose H is negative ; :: thesis: ( len H = 1 + (len (the_argument_of H)) & len (the_argument_of H) < len H )

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

end;

suppose H is next ; :: thesis: ( len H = 1 + (len (the_argument_of H)) & len (the_argument_of H) < len H )

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

end;

end;