theorem :: ZF_LANG1:63

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