theorem Th9: :: ZF_LANG:9

for H being ZF-formula holds
( H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal )