let H be ZF-formula; :: thesis: ( H is atomic iff Subformulae H = {H} )
thus ( H is atomic implies Subformulae H = {H} ) :: thesis: ( Subformulae H = {H} implies H is atomic )

proof

assume H is atomic ; :: thesis: Subformulae H = {H}
then ( H is being_equality or H is being_membership ) ;
then ( H = (Var1 H) '=' (Var2 H) or H = (Var1 H) 'in' (Var2 H) ) by Th36, Th37;
hence Subformulae H = {H} by Th80, Th81; :: thesis: verum

end;

assume A1: Subformulae H = {H} ; :: thesis: 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 Th61;
then the_argument_of H is_subformula_of H ;
then A4: the_argument_of H in Subformulae H by Def42;
len (the_argument_of H) <> len H by A3, Th60;
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 Th61;
then the_left_argument_of H is_subformula_of H ;
then A7: the_left_argument_of H in Subformulae H by Def42;
len (the_left_argument_of H) <> len H by A6, Th60;
hence contradiction by A1, A7, TARSKI:def 1; :: thesis: verum

end;

assume not H is atomic ; :: thesis: contradiction
then ( H is negative or H is conjunctive or H is universal ) by Th10;
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 Def30, Th40, Th44;
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 Th61;
then the_scope_of H is_subformula_of H ;
then A9: the_scope_of H in Subformulae H by Def42;
len (the_scope_of H) <> len H by A8, Th60;
hence contradiction by A1, A9, TARSKI:def 1; :: thesis: verum