for n being Nat
for R being Relation holds
( dom (iter (R,n)) c= field R & rng (iter (R,n)) c= field R )