let H be ZF-formula; :: thesis: ( H is atomic or H is negative or H is conjunctive or H is universal )
assume ( not H is being_equality & not H is being_membership ) ; :: according to ZF_LANG:def 15 :: thesis: ( H is negative or H is conjunctive or H is universal )
hence ( H is negative or H is conjunctive or H is universal ) by Th25; :: thesis: verum