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 A1: 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 A1, Lm30;
for x, y being object 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 object ; :: 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 A2: ( 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
A3: ( x = p1 & g1 in G & p1 = (iter (g1,n)) . (Bottom P) ) by A1, Lm28;
consider p2 being Element of P, g2 being continuous Function of P,P such that
A4: ( y = p2 & g2 in G & p2 = (iter (g2,n)) . (Bottom P) ) by A1, A2, Lm28;
per cases ( g1 <= g2 or g2 <= g1 ) by A3, A4, Lm31;
suppose g1 <= g2 ; :: thesis: ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P )
then p1 <= p2 by Lm7, A3, A4;
hence ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by A3, A4, ORDERS_2:def 5; :: 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 Lm7, A3, A4;
hence ( [x,y] in the InternalRel of P or [y,x] in the InternalRel of P ) by A3, A4, ORDERS_2:def 5; :: thesis: verum
end;
end;
end;
then A5: the InternalRel of P is_connected_in X by RELAT_2:def 6;
for x being object st x in X holds
[x,x] in the InternalRel of P
proof
let x be object ; :: 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 5; :: 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 A5, ORDERS_1:7;
hence X is non empty Chain of P by ORDERS_2:def 7; :: thesis: verum