let H be ZF-formula; :: thesis: Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}

now

let a be set ; :: thesis: ( ( a in Subformulae ('not' H) implies a in (Subformulae H) \/ {('not' H)} ) & ( a in (Subformulae H) \/ {('not' H)} implies a in Subformulae ('not' H) ) )

A1: now

assume a in {('not' H)} ; :: thesis: a in Subformulae ('not' H)
then A2: a = 'not' H by TARSKI:def 1;
'not' H is_subformula_of 'not' H by Th79;
hence a in Subformulae ('not' H) by A2, Def42; :: thesis: verum

end;

thus ( a in Subformulae ('not' H) implies a in (Subformulae H) \/ {('not' H)} ) :: thesis: ( a in (Subformulae H) \/ {('not' H)} implies a in Subformulae ('not' H) )

proof

assume a in Subformulae ('not' H) ; :: thesis: a in (Subformulae H) \/ {('not' H)}
then consider F being ZF-formula such that
A3: F = a and
A4: F is_subformula_of 'not' H by Def42;

now

assume F <> 'not' H ; :: thesis: a in Subformulae H
then F is_proper_subformula_of 'not' H by A4, Def41;
then F is_subformula_of H by Th90;
hence a in Subformulae H by A3, Def42; :: thesis: verum

end;

then ( a in Subformulae H or a in {('not' H)} ) by A3, TARSKI:def 1;
hence a in (Subformulae H) \/ {('not' H)} by XBOOLE_0:def 3; :: thesis: verum

end;

A5: now

assume a in Subformulae H ; :: thesis: a in Subformulae ('not' H)
then consider F being ZF-formula such that
A6: F = a and
A7: F is_subformula_of H by Def42;
H is_immediate_constituent_of 'not' H by Th71;
then H is_proper_subformula_of 'not' H by Th82;
then H is_subformula_of 'not' H by Def41;
then F is_subformula_of 'not' H by A7, Th86;
hence a in Subformulae ('not' H) by A6, Def42; :: thesis: verum

end;

assume a in (Subformulae H) \/ {('not' H)} ; :: thesis: a in Subformulae ('not' H)
hence a in Subformulae ('not' H) by A5, A1, XBOOLE_0:def 3; :: thesis: verum

end;

hence Subformulae ('not' H) = (Subformulae H) \/ {('not' H)} by TARSKI:1; :: thesis: verum