defpred S1[ ZF-formula] means variables_in $1 <> {} ;
A1:
for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
A2:
for H being ZF-formula
for x being Variable st S1[H] holds
S1[ All (x,H)]
A3:
for x, y being Variable holds
( S1[x '=' y] & S1[x 'in' y] )
A4:
for H being ZF-formula st S1[H] holds
S1[ 'not' H]
by Th140;
for H being ZF-formula holds S1[H]
from ZF_LANG1:sch 1(A3, A4, A1, A2);
then reconsider D = variables_in H as non empty set ;
D c= VAR
proof
let a be
object ;
TARSKI:def 3 ( not a in D or a in VAR )
A5:
rng H c= NAT
by FINSEQ_1:def 4;
A6:
0 + 1
= 1
;
assume A7:
a in D
;
a in VAR
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
;
verum
end;
hence
variables_in H is non empty Subset of VAR
; verum