let V be ManySortedSet of ; :: thesis: ( V . 0 = { [{} ,i] where i is Element of NAT : verum } & ( 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 } ) implies for A being finite Subset of Vars ex i being Element of NAT st A c= V . i )
assume that
A1: V . 0 = { [{} ,i] where i is Element of NAT : verum } and
A2: 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 } ; :: thesis: for A being finite Subset of Vars ex i being Element of NAT st A c= V . i
let A be finite Subset of Vars ; :: thesis: ex i being Element of NAT st A c= V . i
A3: Vars = Union V by A1, A2, VARSdef;
defpred S₁[ set , set ] means $1 in V . $2;

A4: now

let x be set ; :: thesis: ( x in A implies ex i being set st
( i in NAT & S₁[x,i] ) )
assume x in A ; :: thesis: ex i being set st
( i in NAT & S₁[x,i] )
then consider Y being set such that
A5: ( x in Y & Y in rng V ) by A3, TARSKI:def 4;
consider i being set such that
A6: ( i in dom V & Y = V . i ) by A5, FUNCT_1:def 5;
take i = i; :: thesis: ( i in NAT & S₁[x,i] )
thus ( i in NAT & S₁[x,i] ) by A5, A6, PARTFUN1:def 4; :: thesis: verum

end;

consider f being Function such that
A8: ( dom f = A & rng f c= NAT ) and
A9: for x being set st x in A holds
S₁[x,f . x] from WELLORD2:sch 1(A4);

per cases ( A = {} or A <> {} ) ;

suppose A = {} ; :: thesis: ex i being Element of NAT st A c= V . i

then A c= V . 0 by XBOOLE_1:2;
hence ex i being Element of NAT st A c= V . i ; :: thesis: verum

end;

suppose A <> {} ; :: thesis: ex i being Element of NAT st A c= V . i

then reconsider B = rng f as non empty finite Subset of NAT by A8, FINSET_1:26, RELAT_1:65;
reconsider i = max B as Element of NAT by ORDINAL1:def 13;
take i ; :: thesis: A c= V . i
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in V . i )
assume B1: x in A ; :: thesis: x in V . i
then B2: f . x in B by A8, FUNCT_1:def 5;
then reconsider j = f . x as Element of NAT ;
j <= i by B2, XXREAL_2:def 8;
then ( V . j c= V . i & x in V . j ) by A1, A2, A9, B1, Lem1;
hence x in V . i ; :: thesis: verum

end;

end;