let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A holds
( ( H = VERUM A or H is atomic ) iff Subformulae H = {H} )
let H be Element of QC-WFF A; :: thesis: ( ( H = VERUM A or H is atomic ) iff Subformulae H = {H} )
( H is atomic implies Subformulae H = {H} ) by Th86;
hence ( ( H = VERUM A or H is atomic ) implies Subformulae H = {H} ) by Th85; :: thesis: ( not Subformulae H = {H} or H = VERUM A or H is atomic )
assume A1: Subformulae H = {H} ; :: thesis: ( H = VERUM A or H is atomic )

A2: now :: thesis: not H = 'not' (the_argument_of H)

assume H = 'not' (the_argument_of H) ; :: thesis: contradiction
then A3: the_argument_of H is_immediate_constituent_of H ;
then the_argument_of H is_proper_subformula_of H by Th53;
then the_argument_of H is_subformula_of H ;
then A4: the_argument_of H in Subformulae H by Def22;
len (@ (the_argument_of H)) <> len (@ H) by A3, Th51;
hence contradiction by A1, A4, TARSKI:def 1; :: thesis: verum

end;

A5: now :: thesis: not H = (the_left_argument_of H) '&' (the_right_argument_of H)

assume H = (the_left_argument_of H) '&' (the_right_argument_of H) ; :: thesis: contradiction
then A6: the_left_argument_of H is_immediate_constituent_of H ;
then the_left_argument_of H is_proper_subformula_of H by Th53;
then the_left_argument_of H is_subformula_of H ;
then A7: the_left_argument_of H in Subformulae H by Def22;
len (@ (the_left_argument_of H)) <> len (@ H) by A6, Th51;
hence contradiction by A1, A7, TARSKI:def 1; :: thesis: verum

end;

assume ( H <> VERUM A & not H is atomic ) ; :: thesis: contradiction
then ( H is negative or H is conjunctive or H is universal ) by QC_LANG1:9;
then ( H = 'not' (the_argument_of H) or H = (the_left_argument_of H) '&' (the_right_argument_of H) or H = All ((bound_in H),(the_scope_of H)) ) by Th3, Th6, QC_LANG1:def 24;
then A8: the_scope_of H is_immediate_constituent_of H by A2, A5;
then the_scope_of H is_proper_subformula_of H by Th53;
then the_scope_of H is_subformula_of H ;
then A9: the_scope_of H in Subformulae H by Def22;
len (@ (the_scope_of H)) <> len (@ H) by A8, Th51;
hence contradiction by A1, A9, TARSKI:def 1; :: thesis: verum