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

A1: now :: thesis: for H being ZF-formula st H is universal holds
ex H1 being ZF-formula st (len H1) + 1 <= len H

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

end;

A5: now :: thesis: for H being ZF-formula st H is negative holds
ex H1 being ZF-formula st (len H1) + 1 <= len H

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 ;
take H1 = H1; :: thesis: (len H1) + 1 <= len H
len H = (len <*2*>) + (len H1) by A6, FINSEQ_1:22;
hence (len H1) + 1 <= len H by FINSEQ_1:40; :: thesis: verum

end;

A7: now :: thesis: for H being ZF-formula st H is conjunctive holds
ex H1 being ZF-formula st (len H1) + 1 <= len H

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 ;
take H1 = H1; :: thesis: (len H1) + 1 <= len H
A9: ( len (<*3*> ^ H1) = (len <*3*>) + (len H1) & len <*3*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
len H = (len (<*3*> ^ H1)) + (len F1) by A8, FINSEQ_1:22;
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 Th10;
hence ex H1 being ZF-formula st (len H1) + 1 <= len H by A5, A7, A1; :: thesis: verum