theorem :: QC_LANG3:67
for A being QC-alphabet
for p, q being Element of QC-WFF A holds Fixed (p '&' q) = (Fixed p) \/ (Fixed q) by Th42;