theorem Th59: :: QC_LANG2:59

for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( not G is_proper_subformula_of H or not H is_subformula_of G ) by Th58;