theorem Th67: :: ZF_LANG1:67

for p being ZF-formula
for x, y being Variable holds Free (All (x,y,p)) = (Free p) \ {x,y}