set IT = { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } ;
not { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } is empty

proof

(iter (g,0)) . p = p by Lm1;
then p in { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } ;
hence not { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } is empty ; :: thesis: verum

end;

hence { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } is non empty set ; :: thesis: verum