theorem :: QC_LANG2:92

for A being QC-alphabet
for F, G being Element of QC-WFF A holds Subformulae (F 'or' G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&' ('not' G)),(F 'or' G)}