theorem Th13: :: ZF_LANG:13

for H being ZF-formula holds 3 <= len H