let H be Element of QC-WFF ; :: thesis: for x being bound_QC-variable holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
let x be bound_QC-variable; :: thesis: Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
thus Subformulae (All (x,H)) c= (Subformulae H) \/ {(All (x,H))} :: according to XBOOLE_0:def 10 :: thesis: (Subformulae H) \/ {(All (x,H))} c= Subformulae (All (x,H))

proof

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

now

assume F <> All (x,H) ; :: thesis: a in Subformulae H
then F is_proper_subformula_of All (x,H) by A2, Def22;
then F is_subformula_of H by Th91;
hence a in Subformulae H by A1, Def23; :: thesis: verum

end;

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

end;

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

A4: now

assume a in Subformulae H ; :: thesis: a in Subformulae (All (x,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 All (x,H) by Th63;
then H is_proper_subformula_of All (x,H) by Th73;
then H is_subformula_of All (x,H) by Def22;
then F is_subformula_of All (x,H) by A6, Th77;
hence a in Subformulae (All (x,H)) by A5, Def23; :: thesis: verum

end;

now

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

end;

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