let F, H be ZF-formula; :: thesis: ( H is_immediate_constituent_of F implies len H < len F )

A1: now :: thesis: ( F = 'not' H & H is_immediate_constituent_of F implies len H < len F )

assume F = 'not' H ; :: thesis: ( H is_immediate_constituent_of F implies len H < len F )
then len F = (len <*2*>) + (len H) by FINSEQ_1:22
.= (len H) + 1 by FINSEQ_1:40 ;
hence ( H is_immediate_constituent_of F implies len H < len F ) by NAT_1:13; :: thesis: verum

end;

A2: now :: thesis: ( ex H1 being ZF-formula st
( F = H '&' H1 or F = H1 '&' H ) & H is_immediate_constituent_of F implies len H < len F )

given H1 being ZF-formula such that A3: ( F = H '&' H1 or F = H1 '&' H ) ; :: thesis: ( H is_immediate_constituent_of F implies len H < len F )
A4: len ((<*3*> ^ H1) ^ H) = len (<*3*> ^ (H1 ^ H)) by FINSEQ_1:32
.= (len <*3*>) + (len (H1 ^ H)) by FINSEQ_1:22
.= 1 + (len (H1 ^ H)) by FINSEQ_1:40
.= 1 + ((len H) + (len H1)) by FINSEQ_1:22
.= (1 + (len H)) + (len H1) ;
len ((<*3*> ^ H) ^ H1) = (len (<*3*> ^ H)) + (len H1) by FINSEQ_1:22
.= ((len <*3*>) + (len H)) + (len H1) by FINSEQ_1:22
.= (1 + (len H)) + (len H1) by FINSEQ_1:40 ;
then 1 + (len H) <= len F by A3, A4, NAT_1:11;
hence ( H is_immediate_constituent_of F implies len H < len F ) by NAT_1:13; :: thesis: verum

end;

A5: now :: thesis: ( ex x being Variable st F = All (x,H) & H is_immediate_constituent_of F implies len H < len F )

given x being Variable such that A6: F = All (x,H) ; :: thesis: ( H is_immediate_constituent_of F implies len H < len F )
len F = (len (<*4*> ^ <*x*>)) + (len H) by A6, FINSEQ_1:22
.= ((len <*4*>) + (len <*x*>)) + (len H) by FINSEQ_1:22
.= (1 + (len <*x*>)) + (len H) by FINSEQ_1:40
.= (1 + 1) + (len H) by FINSEQ_1:40
.= (1 + (len H)) + 1 ;
then 1 + (len H) <= len F by NAT_1:11;
hence ( H is_immediate_constituent_of F implies len H < len F ) by NAT_1:13; :: thesis: verum

end;

assume H is_immediate_constituent_of F ; :: thesis: len H < len F
hence len H < len F by A1, A2, A5; :: thesis: verum