let H be ZF-formula; ( ( 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 ) )
( H . 1 = 0 or H . 1 = 1 or H . 1 = 2 or H . 1 = 3 or H . 1 = 4 )
by ZF_LANG:40;
hence
( ( 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 ) )
by ZF_LANG:35, ZF_LANG:36, ZF_LANG:37, ZF_LANG:38, ZF_LANG:39; verum