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;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Vars or x in Rank omega )
assume x in Vars ; :: thesis: x in Rank omega
then consider i being set such that
A4: ( i in dom V & x in V . i ) by A1, CARD_5:10;
reconsider i = i as Element of NAT by A4, PARTFUN1:def 4;
defpred S₁[ Nat] means V . $1 c= Rank omega ;
A5: S₁[ 0 ]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in V . 0 or x in Rank omega )
assume x in V . 0 ; :: thesis: x in Rank omega
then consider i being Element of NAT such that
B1: x = [{} ,i] by A2;
i + 1 = succ i by NAT_1:39;
then B3: ( {} c= i & i in i + 1 ) by ORDINAL1:10;
then ( {} in i + 1 & the_rank_of {} = {} & the_rank_of i = i ) by CLASSES1:81, ORDINAL1:22;
then ( {} in Rank (i + 1) & i in Rank (i + 1) ) by B3, CLASSES1:74;
then B2: x in Rank (succ (succ (i + 1))) by B1, CLASSES1:51;
succ (succ (i + 1)) c= omega ;
then Rank (succ (succ (i + 1))) c= Rank omega by CLASSES1:43;
hence x in Rank omega by B2; :: thesis: verum

end;

A6: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume C1: S₁[n] ; :: thesis: S₁[n + 1]
C2: V . (n + 1) = { [(varcl a),j] where a is Subset of (V . n), j is Element of NAT : a is finite } by A3;
thus S₁[n + 1] :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in V . (n + 1) or x in Rank omega )
assume x in V . (n + 1) ; :: thesis: x in Rank omega
then consider a being Subset of (V . n), j being Element of NAT such that
C3: ( x = [(varcl a),j] & a is finite ) by C2;
a c= Rank omega by C1, XBOOLE_1:1;
then a in Rank omega by C3, Lem6;
then reconsider i = the_rank_of a as Element of NAT by CLASSES1:74;
reconsider k = j \/ i as Element of NAT by ORDINAL3:15;
C5: ( the_rank_of (varcl a) = i & the_rank_of j = j ) by Lem5, CLASSES1:81;
( i c= k & j c= k & k in succ k ) by ORDINAL1:10, XBOOLE_1:7;
then ( i in succ k & j in succ k & succ k = k + 1 ) by NAT_1:39, ORDINAL1:22;
then ( varcl a in Rank (k + 1) & j in Rank (k + 1) ) by C5, CLASSES1:74;
then C6: x in Rank (succ (succ (k + 1))) by C3, CLASSES1:51;
succ (succ (k + 1)) c= omega ;
then Rank (succ (succ (k + 1))) c= Rank omega by CLASSES1:43;
hence x in Rank omega by C6; :: thesis: verum

end;

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A6);
then V . i c= Rank omega ;
hence x in Rank omega by A4; :: thesis: verum