theorem :: QC_LANG2:93

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