theorem Th23: :: ZF_LANG:23

for H being ZF-formula holds
( ( H is being_equality & H . 1 = 0 ) or ( H is being_membership & H . 1 = 1 ) or ( H is negative & H . 1 = 2 ) or ( H is conjunctive & H . 1 = 3 ) or ( H is universal & H . 1 = 4 ) )