theorem Th64: :: ZF_LANG1:64

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