theorem :: QC_LANG2:84

for A being QC-alphabet
for G, H being Element of QC-WFF A st G in Subformulae H holds
Subformulae G c= Subformulae H by Th82, Th83;