let H be ZF-formula; :: thesis: ( ( 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 ) )

per cases ( H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal ) by Th9;

case H is being_equality ; :: thesis: H . 1 = 0

hence H . 1 = 0 by Th18; :: thesis: verum

end;

case H is being_membership ; :: thesis: H . 1 = 1

hence H . 1 = 1 by Th19; :: thesis: verum

end;

case H is negative ; :: thesis: H . 1 = 2

hence H . 1 = 2 by Th20; :: thesis: verum

end;

case H is conjunctive ; :: thesis: H . 1 = 3

hence H . 1 = 3 by Th21; :: thesis: verum

end;

case H is universal ; :: thesis: H . 1 = 4

hence H . 1 = 4 by Th22; :: thesis: verum

end;

end;