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_proper_subformula_of G )
let G, H be Element of QC-WFF A; :: thesis: ( not G is_proper_subformula_of H or not H is_proper_subformula_of G )
assume that
A1: G is_subformula_of H and
G <> H and
A2: H is_proper_subformula_of G ; :: according to QC_LANG2:def 21 :: thesis: contradiction
thus contradiction by A1, A2, Th59; :: thesis: verum