let G, H be Element of QC-WFF ; :: thesis: ( not G is_proper_subformula_of H or not H is_immediate_constituent_of G )
assume that
A1: G is_subformula_of H and
G <> H and
A2: H is_immediate_constituent_of G ; :: according to QC_LANG2:def 21 :: thesis: contradiction
thus contradiction by A1, A2, Th73, Th79; :: thesis: verum