let H be ZF-formula; :: thesis: variables_in H is finite
variables_in H = (rng H) \ {0 ,1,2,3,4} by ZF_LANG1:def 3;
hence variables_in H is finite ; :: thesis: verum