theorem Th12: :: ZF_LANG:12

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