theorem Th19: :: MMLQUER2:19

for X being set
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) <> {} ) )