theorem Th1: :: ZFMODEL2:1

for x, y being Variable
for H being ZF-formula holds Free (H / (x,y)) c= ((Free H) \ {x}) \/ {y}