consider f being Function of X,NAT such that
A1: iteration_of O = value_of f and
for x being Element of X st x in X holds
ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) by Def10;
thus ( iteration_of O is antisymmetric & iteration_of O is transitive & iteration_of O is beta-transitive ) by A1; :: thesis: verum