let x be Variable; :: thesis:
let H be ZF-formula; :: thesis:

let a be object ; :: thesis:

A1: now :: thesis:

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

end;

thus ( a in Subformulae (All (x,H)) implies a in (Subformulae H) \/ {(All (x,H))} ) :: thesis:

assume a in Subformulae (All (x,H)) ; :: thesis:
then consider F being ZF-formula such that
A3: F = a and
A4: F is_subformula_of All (x,H) by Def42;

assume F <> All (x,H) ; :: thesis:
then F is_proper_subformula_of All (x,H) by A4;
then F is_subformula_of H by Th71;
hence a in Subformulae H by A3, Def42; :: thesis:

end;

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

end;

A5: now :: thesis:

assume a in Subformulae H ; :: thesis:
then consider F being ZF-formula such that
A6: F = a and
A7: F is_subformula_of H by Def42;
H is_immediate_constituent_of All (x,H) ;
then H is_proper_subformula_of All (x,H) by Th61;
then H is_subformula_of All (x,H) ;
then F is_subformula_of All (x,H) by A7, Th65;
hence a in Subformulae (All (x,H)) by A6, Def42; :: thesis:

end;

assume a in (Subformulae H) \/ {(All (x,H))} ; :: thesis:
hence a in Subformulae (All (x,H)) by A5, A1, XBOOLE_0:def 3; :: thesis:

end;

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