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 Subset 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 Subset 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 Subset 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 Subset 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 Subset of P
consider g being object such that
A2: g in G by XBOOLE_0:def 1;
reconsider g = g as Element of (ConPoset (P,P)) by A2;
reconsider gg = g as continuous Function of P,P by Lm24;
reconsider p = (iter (gg,n)) . (Bottom P) as Element of P ;
A3: p in X by A1, A2;
for x being object st x in X holds
x in the carrier of P

proof

let x be object ; :: thesis: ( x in X implies x in the carrier of P )
assume x in X ; :: thesis: x in the carrier of P
then x is Element of the carrier of P by Lm29, A1;
hence x in the carrier of P ; :: thesis: verum

end;

hence X is non empty Subset of P by A3, TARSKI:def 3; :: thesis: verum