let H be ZF-formula; :: thesis: ( H is atomic or ex H1 being ZF-formula st (len H1) + 1 <= len H )

A1: 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
A2: H = All x,H1 by Def14;
take H1 = H1; :: thesis: (len H1) + 1 <= len H
A3: ( len <*4,x*> = 2 & <*4*> ^ <*x*> = <*4,x*> ) by FINSEQ_1:61, FINSEQ_1:def 9;
A4: (1 + 1) + (len H1) = 1 + (1 + (len H1)) ;
len H = (len (<*4*> ^ <*x*>)) + (len H1) by A2, FINSEQ_1:35;
hence (len H1) + 1 <= len H by A3, A4, NAT_1:11; :: thesis: verum

end;

A5: 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
A6: H = 'not' H1 by Def12;
take H1 = H1; :: thesis: (len H1) + 1 <= len H
len H = (len <*2*>) + (len H1) by A6, FINSEQ_1:35;
hence (len H1) + 1 <= len H by FINSEQ_1:57; :: thesis: verum

end;

A7: 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
A8: H = H1 '&' F1 by Def13;
take H1 = H1; :: thesis: (len H1) + 1 <= len H
A9: ( len (<*3*> ^ H1) = (len <*3*>) + (len H1) & len <*3*> = 1 ) by FINSEQ_1:35, FINSEQ_1:57;
len H = (len (<*3*> ^ H1)) + (len F1) by A8, FINSEQ_1:35;
hence (len H1) + 1 <= len H by A9, NAT_1:11; :: thesis: verum

end;

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