let A be QC-alphabet ; :: thesis: for G, H being Element of QC-WFF A holds
( not G is_proper_subformula_of H or not H is_subformula_of G )
let G, H be Element of QC-WFF A; :: 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 Th58; :: thesis: verum