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;