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