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;
let x be object ; :: 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 object such that
A4: i in dom V and
A5: x in V . i by A1, CARD_5:2;
reconsider i = i as Element of NAT by A4;
defpred S₁[ Nat] means V . $1 c= Rank omega;
A6: S₁[ 0 ]

proof

let x be object ; :: 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
A7: x = [{},i] by A2;
A8: Segm (i + 1) = succ (Segm i) by NAT_1:38;
A9: {} c= i ;
A10: i in i + 1 by A8, ORDINAL1:6;
A11: {} in i + 1 by A8, A9, ORDINAL1:6, ORDINAL1:12;
A12: the_rank_of {} = {} by CLASSES1:73;
A13: the_rank_of i = i by CLASSES1:73;
A14: {} in Rank (i + 1) by A11, A12, CLASSES1:66;
i in Rank (i + 1) by A10, A13, CLASSES1:66;
then A15: x in Rank (succ (succ (i + 1))) by A7, A14, CLASSES1:45;
succ (succ (i + 1)) c= omega ;
then Rank (succ (succ (i + 1))) c= Rank omega by CLASSES1:37;
hence x in Rank omega by A15; :: thesis: verum

end;

A16: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A17: S₁[n] ; :: thesis: S₁[n + 1]
A18: 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 object ; :: 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
A19: x = [(varcl a),j] and
A20: a is finite by A18;
a c= Rank omega by A17, XBOOLE_1:1;
then a in Rank omega by A20, Th22;
then reconsider i = the_rank_of a as Element of NAT by CLASSES1:66;
reconsider k = j \/ i as Element of NAT by ORDINAL3:12;
A21: the_rank_of (varcl a) = i by Th21;
A22: the_rank_of j = j by CLASSES1:73;
A23: k in succ k by ORDINAL1:6;
then A24: i in succ k by ORDINAL1:12, XBOOLE_1:7;
A25: j in succ k by A23, ORDINAL1:12, XBOOLE_1:7;
A26: succ (Segm k) = Segm (k + 1) by NAT_1:38;
then A27: varcl a in Rank (k + 1) by A21, A24, CLASSES1:66;
j in Rank (k + 1) by A22, A25, A26, CLASSES1:66;
then A28: x in Rank (succ (succ (k + 1))) by A19, A27, CLASSES1:45;
succ (succ (k + 1)) c= omega ;
then Rank (succ (succ (k + 1))) c= Rank omega by CLASSES1:37;
hence x in Rank omega by A28; :: thesis: verum

end;

end;

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