theorem Th141: :: ZF_LANG1:141

for H1, H2 being ZF-formula holds variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2)