consider V being ManySortedSet of 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 VARSdef;
defpred S₁[ Nat] means varcl (V . $1) = V . $1;

now

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 ZFMISC_1:33;
hence x c= V . 0 by XBOOLE_1:2; :: thesis: verum

end;

then ( varcl (V . 0 ) c= V . 0 & V . 0 c= varcl (V . 0 ) ) by VARCL;
then B1: S₁[ 0 ] by XBOOLE_0:def 10;

B2: now

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

now

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
B5: ( [x,y] = [(varcl A),j] & A is finite ) by B4;
( x = varcl A & i <= i + 1 ) by B5, NAT_1:11, ZFMISC_1:33;
then ( x c= V . i & V . i' c= V . (i' + 1) ) by A2, A3, B3, Th13, Lem1;
hence x c= V . (i + 1) by XBOOLE_1:1; :: thesis: verum

end;

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

end;

B3: for i being Nat holds S₁[i] from NAT_1:sch 2(B1, B2);
A4: varcl Vars = union { (varcl a) where a is Element of rng V : verum } by A1, Th14;

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

let x be set ; :: 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
A5: ( x in Y & Y in { (varcl a) where a is Element of rng V : verum } ) by A4, TARSKI:def 4;
consider a being Element of rng V such that
A6: Y = varcl a by A5;
consider i being set such that
A7: ( i in dom V & a = V . i ) by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A7, PARTFUN1:def 4;
varcl (V . i) = a by B3, A7;
hence x in Vars by A1, A5, A6, A7, CARD_5:10; :: thesis: verum

end;

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