consider V being ManySortedSet of NAT such that
A1: Vars = Union V and
A2: V . 0 = { [{},i] where i is Element of NAT : verum } and
A3: for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } by Def2;
defpred S₁[ Nat] means varcl (V . $1) = V . $1;

now :: thesis: for x, y being set st [x,y] in V . 0 holds
x c= V . 0

let x, y be set ; :: thesis: ( [x,y] in V . 0 implies x c= V . 0 )
assume [x,y] in V . 0 ; :: thesis: x c= V . 0
then ex i being Element of NAT st [x,y] = [{},i] by A2;
then x = {} by XTUPLE_0:1;
hence x c= V . 0 ; :: thesis: verum

end;

then A4: varcl (V . 0) c= V . 0 by Def1;
V . 0 c= varcl (V . 0) by Def1;
then A5: S₁[ 0 ] by A4, XBOOLE_0:def 10;

A6: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A7: S₁[i] ; :: thesis: S₁[i + 1]
reconsider i9 = i as Element of NAT by ORDINAL1:def 12;
A8: V . (i + 1) = { [(varcl A),j] where A is Subset of (V . i), j is Element of NAT : A is finite } by A3;

now :: thesis: for x, y being set st [x,y] in V . (i + 1) holds
x c= V . (i + 1)

let x, y be set ; :: thesis: ( [x,y] in V . (i + 1) implies x c= V . (i + 1) )
assume [x,y] in V . (i + 1) ; :: thesis: x c= V . (i + 1)
then consider A being Subset of (V . i), j being Element of NAT such that
A9: [x,y] = [(varcl A),j] and
A is finite by A8;
x = varcl A by A9, XTUPLE_0:1;
then A10: x c= V . i by A7, Th9;
V . i9 c= V . (i9 + 1) by A2, A3, Th14, NAT_1:11;
hence x c= V . (i + 1) by A10; :: thesis: verum

end;

then A11: varcl (V . (i + 1)) c= V . (i + 1) by Def1;
V . (i + 1) c= varcl (V . (i + 1)) by Def1;
hence S₁[i + 1] by A11, XBOOLE_0:def 10; :: thesis: verum

end;

A12: for i being Nat holds S₁[i] from NAT_1:sch 2(A5, A6);
A13: varcl Vars = union { (varcl a) where a is Element of rng V : verum } by A1, Th10;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Vars c= varcl Vars

let x be object ; :: thesis: ( x in varcl Vars implies x in Vars )
assume x in varcl Vars ; :: thesis: x in Vars
then consider Y being set such that
A14: x in Y and
A15: Y in { (varcl a) where a is Element of rng V : verum } by A13, TARSKI:def 4;
consider a being Element of rng V such that
A16: Y = varcl a by A15;
consider i being object such that
A17: i in dom V and
A18: a = V . i by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A17;
varcl (V . i) = a by A12, A18;
hence x in Vars by A1, A14, A16, A17, A18, CARD_5:2; :: thesis: verum

end;

thus Vars c= varcl Vars by Def1; :: thesis: verum