let x be Variable; :: thesis: for H being ZF-formula holds Subformulae (All x,H) = (Subformulae H) \/ {(All x,H)}
let H be ZF-formula; :: thesis: Subformulae (All x,H) = (Subformulae H) \/ {(All x,H)}

now

let a be set ; :: thesis: ( ( a in Subformulae (All x,H) implies a in (Subformulae H) \/ {(All x,H)} ) & ( a in (Subformulae H) \/ {(All x,H)} implies a in Subformulae (All x,H) ) )
thus ( a in Subformulae (All x,H) implies a in (Subformulae H) \/ {(All x,H)} ) :: thesis: ( a in (Subformulae H) \/ {(All x,H)} implies a in Subformulae (All x,H) )

proof

assume a in Subformulae (All x,H) ; :: thesis: a in (Subformulae H) \/ {(All x,H)}
then consider F being ZF-formula such that
A1: ( F = a & F is_subformula_of All x,H ) by Def42;

now

assume F <> All x,H ; :: thesis: a in Subformulae H
then F is_proper_subformula_of All x,H by A1, Def41;
then F is_subformula_of H by Th92;
hence a in Subformulae H by A1, Def42; :: 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;

assume A2: a in (Subformulae H) \/ {(All x,H)} ; :: thesis: a in Subformulae (All x,H)

A3: now

assume a in Subformulae H ; :: thesis: a in Subformulae (All x,H)
then consider F being ZF-formula such that
A4: ( F = a & F is_subformula_of H ) by Def42;
H is_immediate_constituent_of All x,H by Th73;
then H is_proper_subformula_of All x,H by Th82;
then H is_subformula_of All x,H by Def41;
then F is_subformula_of All x,H by A4, Th86;
hence a in Subformulae (All x,H) by A4, Def42; :: thesis: verum

end;

now

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

end;

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

end;

hence Subformulae (All x,H) = (Subformulae H) \/ {(All x,H)} by TARSKI:2; :: thesis: verum