theorem :: QC_LANG3:57

for A being QC-alphabet
for p, q being Element of QC-WFF A holds Free (p '&' q) = (Free p) \/ (Free q) by Th42;