:: deftheorem defines iterSet POSET_1:def 2 :
for P being non empty Poset
for g being monotone Function of P,P
for p being Element of P holds iterSet (g,p) = { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } ;