theorem Th10: :: ZF_LANG:10

for H being ZF-formula holds
( H is atomic or H is negative or H is conjunctive or H is universal ) by Th9;