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, ZF_LANG:16;
hence Free (All x,p) = (Free p) \ {x} by A1, ZF_MODEL:1; :: thesis: verum