theorem Th3: :: ZFMODEL2:3

for H being ZF-formula holds
( 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 )