for H being ZF-formula holds
( H is atomic or ex H1 being ZF-formula st (len H1) + 1 <= len H )