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