let P be non empty strict chain-complete Poset; 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)); 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; 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 ; ( 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) ) }
; 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 ;
( 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 )
;
( [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;
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
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; verum