defpred S₁[ ZF-formula] means variables_in $1 <> {} ;
A1: for H1, H2 being ZF-formula st S₁[H1] & S₁[H2] holds
S₁[H1 '&' H2]

let H1, H2 be ZF-formula; :: thesis:
variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2) by Th141;
hence ( S₁[H1] & S₁[H2] implies S₁[H1 '&' H2] ) ; :: thesis:

end;

A2: for H being ZF-formula
for x being Variable st S₁[H] holds
S₁[ All (x,H)]

let H be ZF-formula; :: thesis:
let x be Variable; :: thesis:
variables_in (All (x,H)) = (variables_in H) \/ {x} by Th142;
hence ( S₁[H] implies S₁[ All (x,H)] ) ; :: thesis:

end;

A3: for x, y being Variable holds
( S₁[x '=' y] & S₁[x 'in' y] )

let x, y be Variable; :: thesis:
variables_in (x '=' y) = {x,y} by Th138;
hence ( S₁[x '=' y] & S₁[x 'in' y] ) by Th139; :: thesis:

end;

A4: for H being ZF-formula st S₁[H] holds
S₁[ 'not' H] by Th140;
for H being ZF-formula holds S₁[H] from ZF_LANG1:sch 1(A3, A4, A1, A2);
then reconsider D = variables_in H as non empty set ;
D c= VAR

let a be object ; :: according to TARSKI:def 3 :: thesis:
A5: rng H c= NAT by FINSEQ_1:def 4;
A6: 0 + 1 = 1 ;
assume A7: a in D ; :: thesis:
then a in rng H ;
then reconsider i = a as Element of NAT by A5;
a <> 0 by A7, Th137;
then A8: 1 <= i by A6, NAT_1:13;
A9: 3 + 1 = 4 ;
A10: 2 + 1 = 3 ;
A11: 1 + 1 = 2 ;
a <> 1 by A7, Th137;
then 1 < i by A8, XXREAL_0:1;
then A12: 2 <= i by A11, NAT_1:13;
a <> 2 by A7, Th137;
then 2 < i by A12, XXREAL_0:1;
then A13: 3 <= i by A10, NAT_1:13;
a <> 3 by A7, Th137;
then 3 < i by A13, XXREAL_0:1;
then A14: 4 <= i by A9, NAT_1:13;
a <> 4 by A7, Th137;
then A15: 4 < i by A14, XXREAL_0:1;
4 + 1 = 5 ;
then 5 <= i by A15, NAT_1:13;
hence a in VAR ; :: thesis:

end;

hence variables_in H is non empty Subset of VAR ; :: thesis: