theorem :: ZF_LANG1:65

for p, q being ZF-formula holds Free (p <=> q) = (Free p) \/ (Free q)