theorem Th61: :: ZF_LANG1:61

for p, q being ZF-formula holds Free (p '&' q) = (Free p) \/ (Free q)