let H be ZF-formula; :: thesis: ( H is atomic or ex H1 being ZF-formula st (len H1) + 1 <= len H )
assume not H is atomic ; :: thesis: ex H1 being ZF-formula st (len H1) + 1 <= len H
then A1: ( H is negative or H is conjunctive or H is universal ) by Th26;

A2: now

let H be ZF-formula; :: thesis: ( H is negative implies ex H1 being ZF-formula st (len H1) + 1 <= len H )
assume H is negative ; :: thesis: ex H1 being ZF-formula st (len H1) + 1 <= len H
then consider H1 being ZF-formula such that
A3: H = 'not' H1 by Def12;
take H1 = H1; :: thesis: (len H1) + 1 <= len H
( len H = (len <*2*>) + (len H1) & len <*2*> = 1 & 1 + (len H1) = (len H1) + 1 ) by A3, FINSEQ_1:35, FINSEQ_1:57;
hence (len H1) + 1 <= len H ; :: thesis: verum

end;

A4: now

let H be ZF-formula; :: thesis: ( H is conjunctive implies ex H1 being ZF-formula st (len H1) + 1 <= len H )
assume H is conjunctive ; :: thesis: ex H1 being ZF-formula st (len H1) + 1 <= len H
then consider H1, F1 being ZF-formula such that
A5: H = H1 '&' F1 by Def13;
take H1 = H1; :: thesis: (len H1) + 1 <= len H
( len H = (len (<*3*> ^ H1)) + (len F1) & len (<*3*> ^ H1) = (len <*3*>) + (len H1) & len <*3*> = 1 & 1 + (len H1) = (len H1) + 1 ) by A5, FINSEQ_1:35, FINSEQ_1:57;
hence (len H1) + 1 <= len H by NAT_1:11; :: thesis: verum

end;

now

let H be ZF-formula; :: thesis: ( H is universal implies ex H1 being ZF-formula st (len H1) + 1 <= len H )
assume H is universal ; :: thesis: ex H1 being ZF-formula st (len H1) + 1 <= len H
then consider x being Variable, H1 being ZF-formula such that
A6: H = All x,H1 by Def14;
take H1 = H1; :: thesis: (len H1) + 1 <= len H
( len H = (len (<*4*> ^ <*x*>)) + (len H1) & len <*4,x*> = 2 & <*4*> ^ <*x*> = <*4,x*> & 1 + (len H1) = (len H1) + 1 & (1 + 1) + (len H1) = 1 + (1 + (len H1)) & 1 + (1 + (len H1)) = (1 + (len H1)) + 1 ) by A6, FINSEQ_1:35, FINSEQ_1:61, FINSEQ_1:def 9;
hence (len H1) + 1 <= len H by NAT_1:11; :: thesis: verum

end;

hence ex H1 being ZF-formula st (len H1) + 1 <= len H by A1, A2, A4; :: thesis: verum