theorem :: QC_LANG2:96

for A being QC-alphabet
for H being Element of QC-WFF A st H is conjunctive holds
Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}