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