let H be Element of QC-WFF ; :: thesis: ( ( H = VERUM or H is atomic ) iff Subformulae H = {H} )
( H is atomic implies Subformulae H = {H} )

proof

assume ex k being Element of NAT ex P being QC-pred_symbol of k ex V being QC-variable_list of st H = P ! V ; :: according to QC_LANG1:def 17 :: thesis: Subformulae H = {H}
hence Subformulae H = {H} by Th108; :: thesis: verum

end;

hence ( ( H = VERUM or H is atomic ) implies Subformulae H = {H} ) by Th107; :: thesis: ( not Subformulae H = {H} or H = VERUM or H is atomic )
assume A1: Subformulae H = {H} ; :: thesis: ( H = VERUM or H is atomic )
assume ( H <> VERUM & not H is atomic ) ; :: thesis: contradiction
then ( H is negative or H is conjunctive or H is universal ) by QC_LANG1:33;
then A2: ( 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 Th4, Th7, QC_LANG1:def 23;

A3: now

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

end;

now

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 & the_right_argument_of H is_immediate_constituent_of H ) by Th62;
then ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ) by Th73;
then ( the_left_argument_of H is_subformula_of H & the_right_argument_of H is_subformula_of H ) by Def22;
then A7: ( the_left_argument_of H in Subformulae H & the_right_argument_of H in Subformulae H ) by Def23;
( len (@ (the_left_argument_of H)) <> len (@ H) & len (@ (the_right_argument_of H)) <> len (@ H) ) by A6, Th71;
hence contradiction by A1, A7, TARSKI:def 1; :: thesis: verum

end;

then A8: the_scope_of H is_immediate_constituent_of H by A2, A3, Th63;
then the_scope_of H is_proper_subformula_of H by Th73;
then the_scope_of H is_subformula_of H by Def22;
then A9: the_scope_of H in Subformulae H by Def23;
len (@ (the_scope_of H)) <> len (@ H) by A8, Th71;
hence contradiction by A1, A9, TARSKI:def 1; :: thesis: verum