theorem :: QC_LANG2:75

for A being QC-alphabet
for F, H being Element of QC-WFF A st H is atomic holds
not F is_proper_subformula_of H by Th65;