let H be Element of QC-WFF ; :: thesis: Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}
thus Subformulae ('not' H) c= (Subformulae H) \/ {('not' H)} :: according to XBOOLE_0:def 10 :: thesis: (Subformulae H) \/ {('not' H)} c= Subformulae ('not' H)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Subformulae ('not' H) or a in (Subformulae H) \/ {('not' H)} )
assume a in Subformulae ('not' H) ; :: thesis: a in (Subformulae H) \/ {('not' H)}
then consider F being Element of QC-WFF such that
A1: F = a and
A2: F is_subformula_of 'not' H by Def23;

now

assume F <> 'not' H ; :: thesis: a in Subformulae H
then F is_proper_subformula_of 'not' H by A2, Def22;
then F is_subformula_of H by Th86;
hence a in Subformulae H by A1, Def23; :: thesis: verum

end;

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

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (Subformulae H) \/ {('not' H)} or a in Subformulae ('not' H) )
assume A3: a in (Subformulae H) \/ {('not' H)} ; :: thesis: a in Subformulae ('not' H)

A4: now

assume a in Subformulae H ; :: thesis: a in Subformulae ('not' H)
then consider F being Element of QC-WFF such that
A5: F = a and
A6: F is_subformula_of H by Def23;
H is_immediate_constituent_of 'not' H by Def20;
then H is_proper_subformula_of 'not' H by Th73;
then H is_subformula_of 'not' H by Def22;
then F is_subformula_of 'not' H by A6, Th77;
hence a in Subformulae ('not' H) by A5, Def23; :: thesis: verum

end;

now

assume a in {('not' H)} ; :: thesis: a in Subformulae ('not' H)
then a = 'not' H by TARSKI:def 1;
hence a in Subformulae ('not' H) by Def23; :: thesis: verum

end;

hence a in Subformulae ('not' H) by A3, A4, XBOOLE_0:def 3; :: thesis: verum