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 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: ( 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
A2: ( 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 A1;
thus x is Element of P by A2; :: thesis: verum

end;

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