let G, H be Element of QC-WFF ; :: thesis: ( not G is_proper_subformula_of H or not H is_subformula_of G )
assume ( G is_subformula_of H & G <> H & H is_subformula_of G ) ; :: according to QC_LANG2:def 21 :: thesis: contradiction
hence contradiction by Th78; :: thesis: verum