theorem :: ZF_LANG1:151

for H being ZF-formula holds Free H c= variables_in H