let x be Variable; for H being ZF-formula holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
let H be ZF-formula; Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
now for a being object holds
( ( 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)) ) )let a be
object ;
( ( 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))} )
( a in (Subformulae H) \/ {(All (x,H))} implies a in Subformulae (All (x,H)) )assume
a in (Subformulae H) \/ {(All (x,H))}
;
a in Subformulae (All (x,H))hence
a in Subformulae (All (x,H))
by A5, A1, XBOOLE_0:def 3;
verum end;
hence
Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
by TARSKI:2; verum