let X be set ; :: thesis: for R being Relation st ( for n being Nat holds (iter (R,n)) .: X <> {} ) & X is finite holds
ex x being set st
( x in X & ( for n being Nat holds Im ((iter (R,n)),x) <> {} ) )
let R be Relation; :: thesis: ( ( for n being Nat holds (iter (R,n)) .: X <> {} ) & X is finite implies ex x being set st
( x in X & ( for n being Nat holds Im ((iter (R,n)),x) <> {} ) ) )
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: contradiction
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] )

proof

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

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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { {x} where x is Element of X : x in X } or z in bool X )
assume z in { {x} where x is Element of X : x in X } ; :: thesis: z in bool X
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: verum

end;

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

proof

thus X c= union Y :: according to XBOOLE_0:def 10 :: thesis: union Y c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in union Y )
assume x in X ; :: thesis: x in union Y
then ( x in {x} & {x} in Y ) by TARSKI:def 1;
hence x in union Y by TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union Y or x in X )
assume x in union Y ; :: thesis: x in X
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: verum

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= {{}}

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { ((iter (R,n)) .: y) where y is Subset of X : y in Y } or z in {{}} )
assume z in { ((iter (R,n)) .: y) where y is Subset of X : y in Y } ; :: thesis: z in {{}}
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: verum

end;

then (iter (R,n)) .: X c= union {{}} by A10, ZFMISC_1:77;
then (iter (R,n)) .: X c= {} by ZFMISC_1:25;
then (iter (R,n)) .: X = {} ;
hence contradiction by A1; :: thesis: verum