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