theorem Th20: :: MMLQUER2:20

for X being set
for R being Relation st R is co-well_founded & R is irreflexive & X is finite & R is finite holds
ex n being Nat st (iter (R,n)) .: X = {}