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
A2: ( x = y & ex n being Nat st y = (iter (g,n)) . (Bottom P) ) ;
thus x is Element of P by A2; :: thesis: verum
end;
for x being object st x in iterSet (g,(Bottom P)) holds
x in the carrier of P
proof
let x be object ; :: 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 object 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 object ; :: 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 A3: ( 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
A4: ( x = p & ex n being Nat st p = (iter (g,n)) . (Bottom P) ) by A3;
consider p1 being Element of P such that
A5: ( y = p1 & ex m being Nat st p1 = (iter (g,m)) . (Bottom P) ) by A3;
consider n being Nat such that
A6: p = (iter (g,n)) . (Bottom P) by A4;
consider m being Nat such that
A7: p1 = (iter (g,m)) . (Bottom P) by A5;
( p <= p1 or p1 <= p )
proof
set a1 = (iter (g,1)) . (Bottom P);
A8: (iter (g,1)) . (Bottom P) = g . (Bottom P) by FUNCT_7:70;
per cases ( n <= m or m <= n ) ;
suppose n <= m ; :: thesis: ( p <= p1 or p1 <= p )
hence ( p <= p1 or p1 <= p ) by A6, A7, A8, Lm5, YELLOW_0:44; :: thesis: verum
end;
suppose m <= n ; :: thesis: ( p <= p1 or p1 <= p )
hence ( p <= p1 or p1 <= p ) by A6, A7, A8, Lm5, YELLOW_0:44; :: thesis: verum
end;
end;
end;
hence ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by A4, A5, ORDERS_2:def 5; :: thesis: verum
end;
then A9: the InternalRel of P is_connected_in L by RELAT_2:def 6;
for x being object st x in L holds
[x,x] in the InternalRel of P
proof
let x be object ; :: 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 5; :: 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 A9, ORDERS_1:7;
then reconsider L = L as Chain of P by ORDERS_2:def 7;
L is non empty Chain of P ;
hence iterSet (g,(Bottom P)) is non empty Chain of P ; :: thesis: verum