let P be non empty strict chain-complete Poset; :: thesis: for g being monotone Function of P,P holds iterSet g,(Bottom P) is non empty Chain of P
let g be monotone Function of P,P; :: thesis: iterSet g,(Bottom P) is non empty Chain of P
set a = Bottom P;
set R = the InternalRel of P;
set L = iterSet g,(Bottom P);
A1: for x being set st x in iterSet g,(Bottom P) holds
x is Element of P

proof

let x be set ; :: thesis: ( x in iterSet g,(Bottom P) implies x is Element of P )
assume x in iterSet g,(Bottom P) ; :: thesis: x is Element of P
then consider y being Element of P such that
B1: ( x = y & ex n being Nat st y = (iter g,n) . (Bottom P) ) ;
thus x is Element of P by B1; :: thesis: verum

end;

for x being set st x in iterSet g,(Bottom P) holds
x in the carrier of P

proof

let x be set ; :: thesis: ( x in iterSet g,(Bottom P) implies x in the carrier of P )
assume x in iterSet g,(Bottom P) ; :: thesis: x in the carrier of P
then x is Element of the carrier of P by A1;
hence x in the carrier of P ; :: thesis: verum

end;

then reconsider L = iterSet g,(Bottom P) as Subset of P by TARSKI:def 3;
for x, y being set st x in L & y in L & x <> y & not [x,y] in the InternalRel of P holds
[y,x] in the InternalRel of P

proof

let x, y be set ; :: thesis: ( x in L & y in L & x <> y & not [x,y] in the InternalRel of P implies [y,x] in the InternalRel of P )
assume B1: ( x in L & y in L & x <> y ) ; :: thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P )
then reconsider x = x, y = y as Element of P ;
consider p being Element of P such that
B2: ( x = p & ex n being Nat st p = (iter g,n) . (Bottom P) ) by B1;
consider p1 being Element of P such that
B3: ( y = p1 & ex m being Nat st p1 = (iter g,m) . (Bottom P) ) by B1;
consider n being Nat such that
B4: p = (iter g,n) . (Bottom P) by B2;
consider m being Nat such that
B5: p1 = (iter g,m) . (Bottom P) by B3;
( p <= p1 or p1 <= p )

proof

set a1 = (iter g,1) . (Bottom P);
C1: (iter g,1) . (Bottom P) = g . (Bottom P) by FUNCT_7:72;

per cases ( n <= m or m <= n ) ;

suppose n <= m ; :: thesis: ( p <= p1 or p1 <= p )

hence ( p <= p1 or p1 <= p ) by B4, B5, C1, YELLOW_0:44, Lemiter15; :: thesis: verum

end;

suppose m <= n ; :: thesis: ( p <= p1 or p1 <= p )

hence ( p <= p1 or p1 <= p ) by B4, B5, C1, YELLOW_0:44, Lemiter15; :: thesis: verum

end;

end;

end;

hence ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by ORDERS_2:def 9, B2, B3; :: thesis: verum

end;

then A1: the InternalRel of P is_connected_in L by RELAT_2:def 6;
for x being set st x in L holds
[x,x] in the InternalRel of P

proof

let x be set ; :: thesis: ( x in L implies [x,x] in the InternalRel of P )
assume x in L ; :: thesis: [x,x] in the InternalRel of P
then reconsider x = x as Element of P ;
x <= x ;
hence [x,x] in the InternalRel of P by ORDERS_2:def 9; :: thesis: verum

end;

then the InternalRel of P is_reflexive_in L by RELAT_2:def 1;
then the InternalRel of P is_strongly_connected_in L by A1, ORDERS_1:92;
then reconsider L = L as Chain of P by ORDERS_2:def 11;
L is non empty Chain of P ;
hence iterSet g,(Bottom P) is non empty Chain of P ; :: thesis: verum