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:23;
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:18, ZF_LANG:19, ZF_LANG:20, ZF_LANG:21, ZF_LANG:22; verum