:: deftheorem defines variables_in ZF_LANG1:def 2 :
for H being ZF-formula holds variables_in H = (rng H) \ {0,1,2,3,4};