let H be ZF-formula; :: thesis: Free H c= variables_in H
defpred S₁[ ZF-formula] means Free $1 c= variables_in $1;
A1: for x, y being Variable holds
( S₁[x '=' y] & S₁[x 'in' y] )

proof

let x, y be Variable; :: thesis: ( S₁[x '=' y] & S₁[x 'in' y] )
( variables_in (x '=' y) = {x,y} & variables_in (x 'in' y) = {x,y} & Free (x '=' y) = {x,y} & Free (x 'in' y) = {x,y} ) by Th63, Th64, Th151, Th152;
hence ( S₁[x '=' y] & S₁[x 'in' y] ) ; :: thesis: verum

end;

A2: for H1 being ZF-formula st S₁[H1] holds
S₁[ 'not' H1]

proof

let H1 be ZF-formula; :: thesis: ( S₁[H1] implies S₁[ 'not' H1] )
assume Free H1 c= variables_in H1 ; :: thesis: S₁[ 'not' H1]
then Free ('not' H1) c= variables_in H1 by Th65;
hence S₁[ 'not' H1] by Th153; :: thesis: verum

end;

A3: for H1, H2 being ZF-formula st S₁[H1] & S₁[H2] holds
S₁[H1 '&' H2]

proof

let H1, H2 be ZF-formula; :: thesis: ( S₁[H1] & S₁[H2] implies S₁[H1 '&' H2] )
assume ( Free H1 c= variables_in H1 & Free H2 c= variables_in H2 ) ; :: thesis: S₁[H1 '&' H2]
then (Free H1) \/ (Free H2) c= (variables_in H1) \/ (variables_in H2) by XBOOLE_1:13;
then Free (H1 '&' H2) c= (variables_in H1) \/ (variables_in H2) by Th66;
hence S₁[H1 '&' H2] by Th154; :: thesis: verum

end;

A4: for H1 being ZF-formula
for x being Variable st S₁[H1] holds
S₁[ All x,H1]

proof

let H1 be ZF-formula; :: thesis: for x being Variable st S₁[H1] holds
S₁[ All x,H1]
let x be Variable; :: thesis: ( S₁[H1] implies S₁[ All x,H1] )
assume A5: Free H1 c= variables_in H1 ; :: thesis: S₁[ All x,H1]
( (Free H1) \ {x} c= Free H1 & variables_in H1 c= (variables_in H1) \/ {x} ) by XBOOLE_1:7, XBOOLE_1:36;
then A6: ( Free (All x,H1) c= Free H1 & variables_in H1 c= variables_in (All x,H1) ) by Th67, Th155;
then Free H1 c= variables_in (All x,H1) by A5, XBOOLE_1:1;
hence S₁[ All x,H1] by A6, XBOOLE_1:1; :: thesis: verum

end;

for H being ZF-formula holds S₁[H] from ZF_LANG1:sch 1(A1, A2, A3, A4);
hence Free H c= variables_in H ; :: thesis: verum