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 S1[ 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
( S1[x '=' y] & S1[x 'in' y] )
proof
let x, y be Variable; :: thesis: ( S1[x '=' y] & S1[x 'in' y] )
consider i being Element of NAT such that
A2: x = x. i by ZF_LANG1:77;
consider j being Element of NAT such that
A3: y = x. j by ZF_LANG1:77;
j <= j + i by NAT_1:11;
then A4: j < (i + j) + 1 by NAT_1:13;
i <= i + j by NAT_1:11;
then A5: i < (i + j) + 1 by NAT_1:13;
A6: variables_in (x '=' y) = {x,y} by ZF_LANG1:138;
thus S1[x '=' y] :: thesis: S1[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 ;
hence k < (i + j) + 1 by ; :: 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 )
A7: variables_in (x 'in' y) = {x,y} by ZF_LANG1:139;
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 ;
hence k < (i + j) + 1 by ; :: thesis: verum
end;
A8: for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
proof
let H1, H2 be ZF-formula; :: thesis: ( S1[H1] & S1[H2] implies S1[H1 '&' H2] )
given i1 being Element of NAT such that A9: for j being Element of NAT st x. j in variables_in H1 holds
j < i1 ; :: thesis: ( not S1[H2] or S1[H1 '&' H2] )
given i2 being Element of NAT such that A10: for j being Element of NAT st x. j in variables_in H2 holds
j < i2 ; :: thesis: S1[H1 '&' H2]
( i1 <= i2 or i1 > i2 ) ;
then consider i being Element of NAT such that
A11: ( ( 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 () \/ () by ZF_LANG1:141;
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 ;
hence j < i by ; :: thesis: verum
end;
A12: for H being ZF-formula
for x being Variable st S1[H] holds
S1[ All (x,H)]
proof
let H be ZF-formula; :: thesis: for x being Variable st S1[H] holds
S1[ All (x,H)]

let x be Variable; :: thesis: ( S1[H] implies S1[ All (x,H)] )
given i1 being Element of NAT such that A13: for j being Element of NAT st x. j in variables_in H holds
j < i1 ; :: thesis: S1[ All (x,H)]
consider i2 being Element of NAT such that
A14: x = x. i2 by ZF_LANG1:77;
( i1 <= i2 + 1 or i1 > i2 + 1 ) ;
then consider i being Element of NAT such that
A15: ( ( 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 () \/ {x} by ZF_LANG1:142;
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 ;
then ( j < i1 or j < i2 + 1 ) by ZF_LANG1:76;
hence j < i by ; :: thesis: verum
end;
A16: for H being ZF-formula st S1[H] holds
S1[ 'not' H]
proof
let H be ZF-formula; :: thesis: ( S1[H] implies S1[ 'not' H] )
variables_in () = variables_in H by ZF_LANG1:140;
hence ( S1[H] implies S1[ 'not' H] ) ; :: thesis: verum
end;
for H being ZF-formula holds S1[H] from ZF_LANG1:sch 1(A1, A16, A8, A12);
then consider i being Element of NAT such that
A17: 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 A17; :: 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 A17; :: thesis: verum