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 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 Th60;
hence S₁[ 'not' H1] by Th140; :: thesis: verum

end;

A2: 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 Th61;
hence S₁[H1 '&' H2] by Th141; :: thesis: verum

end;

A3: 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)] )
(Free H1) \ {x} c= Free H1 by XBOOLE_1:36;
then A4: Free (All (x,H1)) c= Free H1 by Th62;
variables_in H1 c= (variables_in H1) \/ {x} by XBOOLE_1:7;
then A5: variables_in H1 c= variables_in (All (x,H1)) by Th142;
assume Free H1 c= variables_in H1 ; :: thesis: S₁[ All (x,H1)]
then Free H1 c= variables_in (All (x,H1)) by A5;
hence S₁[ All (x,H1)] by A4, XBOOLE_1:1; :: thesis: verum

end;

A6: 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} ) by Th138, Th139;
hence ( S₁[x '=' y] & S₁[x 'in' y] ) by Th58, Th59; :: thesis: verum

end;

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