let H be ZF-formula; :: thesis: ( ex i being Element of NAT st
for j being Element of NAT st x. j in variables_in H holds
j < i & not for x being Variable holds x in variables_in H )
defpred S₁[ ZF-formula] means ex i being Element of NAT st
for j being Element of NAT st x. j in variables_in $1 holds
j < i;
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] )
consider i being Element of NAT such that
A2: x = x. i by ZF_LANG1:87;
consider j being Element of NAT such that
A3: y = x. j by ZF_LANG1:87;
( i <= i + j & j <= j + i & i + j = j + i ) by NAT_1:11;
then A4: ( i < (i + j) + 1 & j < (i + j) + 1 ) by NAT_1:13;
A5: ( variables_in (x '=' y) = {x,y} & variables_in (x 'in' y) = {x,y} ) by ZF_LANG1:151, ZF_LANG1:152;
thus S₁[x '=' y] :: thesis: S₁[x 'in' y]

proof

take (i + j) + 1 ; :: thesis: for j being Element of NAT st x. j in variables_in (x '=' y) holds
j < (i + j) + 1
let k be Element of NAT ; :: thesis: ( x. k in variables_in (x '=' y) implies k < (i + j) + 1 )
assume x. k in variables_in (x '=' y) ; :: thesis: k < (i + j) + 1
then ( x. k = x. i or x. k = x. j ) by A2, A3, A5, TARSKI:def 2;
hence k < (i + j) + 1 by A4, ZF_LANG1:86; :: thesis: verum

end;

take (i + j) + 1 ; :: thesis: for j being Element of NAT st x. j in variables_in (x 'in' y) holds
j < (i + j) + 1
let k be Element of NAT ; :: thesis: ( x. k in variables_in (x 'in' y) implies k < (i + j) + 1 )
assume x. k in variables_in (x 'in' y) ; :: thesis: k < (i + j) + 1
then ( x. k = x. i or x. k = x. j ) by A2, A3, A5, TARSKI:def 2;
hence k < (i + j) + 1 by A4, ZF_LANG1:86; :: thesis: verum

end;

A6: for H being ZF-formula st S₁[H] holds
S₁[ 'not' H]

proof

let H be ZF-formula; :: thesis: ( S₁[H] implies S₁[ 'not' H] )
variables_in ('not' H) = variables_in H by ZF_LANG1:153;
hence ( S₁[H] implies S₁[ 'not' H] ) ; :: thesis: verum

end;

A7: 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] )
given i1 being Element of NAT such that A8: for j being Element of NAT st x. j in variables_in H1 holds
j < i1 ; :: thesis: ( not S₁[H2] or S₁[H1 '&' H2] )
given i2 being Element of NAT such that A9: for j being Element of NAT st x. j in variables_in H2 holds
j < i2 ; :: thesis: S₁[H1 '&' H2]
( i1 <= i2 or i1 > i2 ) ;
then consider i being Element of NAT such that
A10: ( ( i1 <= i2 & i = i2 ) or ( i1 > i2 & i = i1 ) ) ;
take i ; :: thesis: for j being Element of NAT st x. j in variables_in (H1 '&' H2) holds
j < i
let j be Element of NAT ; :: thesis: ( x. j in variables_in (H1 '&' H2) implies j < i )
assume x. j in variables_in (H1 '&' H2) ; :: thesis: j < i
then x. j in (variables_in H1) \/ (variables_in H2) by ZF_LANG1:154;
then ( x. j in variables_in H1 or x. j in variables_in H2 ) by XBOOLE_0:def 3;
then ( j < i1 or j < i2 ) by A8, A9;
hence j < i by A10, XXREAL_0:2; :: thesis: verum

end;

A11: 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] )
given i1 being Element of NAT such that A12: for j being Element of NAT st x. j in variables_in H holds
j < i1 ; :: thesis: S₁[ All x,H]
consider i2 being Element of NAT such that
A13: x = x. i2 by ZF_LANG1:87;
( i1 <= i2 + 1 or i1 > i2 + 1 ) ;
then consider i being Element of NAT such that
A14: ( ( i1 <= i2 + 1 & i = i2 + 1 ) or ( i1 > i2 + 1 & i = i1 ) ) ;
take i ; :: thesis: for j being Element of NAT st x. j in variables_in (All x,H) holds
j < i
let j be Element of NAT ; :: thesis: ( x. j in variables_in (All x,H) implies j < i )
assume x. j in variables_in (All x,H) ; :: thesis: j < i
then x. j in (variables_in H) \/ {x} by ZF_LANG1:155;
then ( x. j in variables_in H or ( x. j in {x} & i2 + 0 = i2 & 0 < 1 ) ) by XBOOLE_0:def 3;
then ( j < i1 or ( x. j = x. i2 & i2 < i2 + 1 ) ) by A12, A13, TARSKI:def 1, XREAL_1:8;
then ( j < i1 or j < i2 + 1 ) by ZF_LANG1:86;
hence j < i by A14, XXREAL_0:2; :: thesis: verum

end;

for H being ZF-formula holds S₁[H] from ZF_LANG1:sch 1(A1, A6, A7, A11);
then consider i being Element of NAT such that
A15: for j being Element of NAT st x. j in variables_in H holds
j < i ;
thus ex i being Element of NAT st
for j being Element of NAT st x. j in variables_in H holds
j < i by A15; :: thesis: not for x being Variable holds x in variables_in H
take x. i ; :: thesis: not x. i in variables_in H
thus not x. i in variables_in H by A15; :: thesis: verum