theorem Th18: :: MMLQUER2:18

for X being set
for R being Relation
for n, m being Nat st (iter (R,n)) .: X = {} & m >= n holds
(iter (R,m)) .: X = {}