defpred S₁[ ZF-formula] means 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} ) by Th151, Th152;
hence ( S₁[x '=' y] & S₁[x 'in' y] ) ; :: thesis: verum

end;

A2: for H being ZF-formula st S₁[H] holds
S₁[ 'not' H] by Th153;
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] )
variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2) by Th154;
hence ( S₁[H1] & S₁[H2] implies S₁[H1 '&' H2] ) ; :: thesis: verum

end;

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

proof

let H be ZF-formula; :: thesis: for x being Variable st S₁[H] holds
S₁[ All x,H]
let x be Variable; :: thesis: ( S₁[H] implies S₁[ All x,H] )
( variables_in (All x,H) = (variables_in H) \/ {x} & {x} <> {} ) by Th155;
hence ( S₁[H] implies S₁[ All x,H] ) ; :: thesis: verum

end;

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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in D or a in VAR )
assume a in D ; :: thesis: a in VAR
then A5: ( a in rng H & rng H c= NAT & a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 ) by Th150, FINSEQ_1:def 4;
then reconsider i = a as Element of NAT ;
( 0 < i & 0 + 1 = 1 ) by A5;
then 1 <= i by NAT_1:13;
then ( 1 < i & 1 + 1 = 2 ) by A5, XXREAL_0:1;
then 2 <= i by NAT_1:13;
then ( 2 < i & 2 + 1 = 3 ) by A5, XXREAL_0:1;
then 3 <= i by NAT_1:13;
then ( 3 < i & 3 + 1 = 4 ) by A5, XXREAL_0:1;
then 4 <= i by NAT_1:13;
then ( 4 < i & 4 + 1 = 5 ) by A5, XXREAL_0:1;
then 5 <= i by NAT_1:13;
hence a in VAR ; :: thesis: verum

end;

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