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: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 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, A6, TARSKI:def 2;
hence k < (i + j) + 1 by A5, A4, ZF_LANG1:76; :: 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 A2, A3, A7, TARSKI:def 2;
hence k < (i + j) + 1 by A5, A4, ZF_LANG1:76; :: thesis: verum

end;

A8: 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 A9: 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 A10: 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
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 (variables_in H1) \/ (variables_in H2) 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 A9, A10;
hence j < i by A11, XXREAL_0:2; :: thesis: verum

end;

A12: 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 A13: 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
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 (variables_in H) \/ {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 A13, A14, TARSKI:def 1, XREAL_1:6;
then ( j < i1 or j < i2 + 1 ) by ZF_LANG1:76;
hence j < i by A15, XXREAL_0:2; :: thesis: verum

end;

A16: 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:140;
hence ( S₁[H] implies S₁[ 'not' H] ) ; :: thesis: verum

end;

for H being ZF-formula holds S₁[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