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 Lemiter10;
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