let p be ZF-formula; :: thesis: for x being Variable holds Free (All (x,p)) = (Free p) \ {x}
let x be Variable; :: thesis: Free (All (x,p)) = (Free p) \ {x}
A1: the_scope_of (All (x,p)) = p by Th8;
( All (x,p) is universal & bound_in (All (x,p)) = x ) by Th8;
hence Free (All (x,p)) = (Free p) \ {x} by A1, ZF_MODEL:1; :: thesis: verum