let P be non empty strict chain-complete Poset; :: thesis: for G being non empty Chain of (ConPoset P,P)
for n being Nat
for X being set st X = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,n) . (Bottom P) ) } holds
X is non empty Chain of P
let G be non empty Chain of (ConPoset P,P); :: thesis: for n being Nat
for X being set st X = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,n) . (Bottom P) ) } holds
X is non empty Chain of P
let n be Nat; :: thesis: for X being set st X = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,n) . (Bottom P) ) } holds
X is non empty Chain of P
let X be set ; :: thesis: ( X = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,n) . (Bottom P) ) } implies X is non empty Chain of P )
assume A0: X = { p where p is Element of P : ex g being Element of (ConPoset P,P) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter h,n) . (Bottom P) ) } ; :: thesis: X is non empty Chain of P
set R = the InternalRel of P;
reconsider X = X as non empty Subset of P by A0, LemFix03;
for x, y being set st x in X & y in X & 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 X & y in X & x <> y & not [x,y] in the InternalRel of P implies [y,x] in the InternalRel of P )
assume B1: ( x in X & y in X & x <> y ) ; :: thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P )
then consider p1 being Element of P, g1 being continuous Function of P,P such that
B2: ( x = p1 & g1 in G & p1 = (iter g1,n) . (Bottom P) ) by A0, LemFix02;
consider p2 being Element of P, g2 being continuous Function of P,P such that
B3: ( y = p2 & g2 in G & p2 = (iter g2,n) . (Bottom P) ) by A0, B1, LemFix02;

per cases ( g1 <= g2 or g2 <= g1 ) by B2, B3, LemFix0401;

suppose g1 <= g2 ; :: thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P )

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

end;

suppose g2 <= g1 ; :: thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P )

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

end;

end;

end;

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

proof

let x be set ; :: thesis: ( x in X implies [x,x] in the InternalRel of P )
assume x in X ; :: 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 X by RELAT_2:def 1;
then the InternalRel of P is_strongly_connected_in X by A1, ORDERS_1:92;
hence X is non empty Chain of P by ORDERS_2:def 11; :: thesis: verum