let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}
let H be Element of QC-WFF A; :: 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 object ; :: 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 A such that
A1: F = a and
A2: F is_subformula_of 'not' H by Def22;

now :: thesis: ( F <> 'not' H implies a in Subformulae H )

assume F <> 'not' H ; :: thesis: a in Subformulae H
then F is_proper_subformula_of 'not' H by A2;
then F is_subformula_of H by Th66;
hence a in Subformulae H by A1, Def22; :: 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 object ; :: 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 :: thesis: ( a in Subformulae H implies a in Subformulae ('not' H) )

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

end;

now :: thesis: ( a in {('not' H)} implies a in Subformulae ('not' H) )

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 Def22; :: thesis: verum

end;

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