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