theorem :: ZF_LANG1:38

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