let X be set ; :: thesis:
let R be Relation; :: thesis:
assume that
A1: for n being Nat holds (iter (R,n)) .: X <> {} and
A2: X is finite and
A3: for x being set st x in X holds
ex n being Nat st Im ((iter (R,n)),x) = {} ; :: thesis:
defpred S₁[ object , object ] means ex n being Nat st
( $2 = n & Im ((iter (R,n)),$1) = {} );
A4: for x being object st x in X holds
ex y being object st
( y in NAT & S₁[x,y] )

let x be object ; :: thesis:
assume x in X ; :: thesis:
then consider n being Nat such that
A5: Im ((iter (R,n)),x) = {} by A3;
take y = n; :: thesis:
thus ( y in NAT & S₁[x,y] ) by A5, ORDINAL1:def 12; :: thesis:

end;

consider f being Function such that
A6: ( dom f = X & rng f c= NAT & ( for x being object st x in X holds
S₁[x,f . x] ) ) from FUNCT_1:sch 6(A4);
reconsider f = f as Function of X,NAT by A6, FUNCT_2:2;
consider n being Nat such that
A7: rng f c= Segm n by A2, AFINSQ_2:2;
{ {x} where x is Element of X : x in X } c= bool X

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { {x} where x is Element of X : x in X } ; :: thesis:
then consider x being Element of X such that
A8: ( z = {x} & x in X ) ;
z is Subset of X by A8, ZFMISC_1:31;
hence z in bool X ; :: thesis:

end;

then reconsider Y = { {x} where x is Element of X : x in X } as Subset-Family of X ;
X = union Y

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union Y ; :: thesis:
then consider z being set such that
A9: ( x in z & z in Y ) by TARSKI:def 4;
thus x in X by A9; :: thesis:

end;

then A10: (iter (R,n)) .: X = union { ((iter (R,n)) .: y) where y is Subset of X : y in Y } by RELSET_2:14;
{ ((iter (R,n)) .: y) where y is Subset of X : y in Y } c= {{}}

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { ((iter (R,n)) .: y) where y is Subset of X : y in Y } ; :: thesis:
then consider y being Subset of X such that
A11: ( z = (iter (R,n)) .: y & y in Y ) ;
consider x being Element of X such that
A12: ( y = {x} & x in X ) by A11;
consider m being Nat such that
A13: ( f . x = m & Im ((iter (R,m)),x) = {} ) by A6, A12;
m in rng f by A6, A12, A13, FUNCT_1:def 3;
then m < n by A7, NAT_1:44;
then z = {} by A11, A12, A13, Th18;
hence z in {{}} by TARSKI:def 1; :: thesis:

end;