let x be set ; :: thesis: for P being 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) ) } & x in X holds
x is Element of P
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) ) } & x in X holds
x is Element 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) ) } & x in X holds
x is Element 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) ) } & x in X holds
x is Element 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) ) } & x in X implies x is Element 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: ( not x in X or x is Element of P )
( x in X implies x is Element of P )

proof

assume x in X ; :: thesis: x is Element of P
then consider p being Element of P such that
B1: ( x = 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) ) ) by A0;
thus x is Element of P by B1; :: thesis: verum

end;

hence ( not x in X or x is Element of P ) ; :: thesis: verum