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, 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
ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) )
let G be non empty Chain of (ConPoset (P,P)); :: thesis: for n being Nat
for X, 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
ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) )
let n be Nat; :: thesis: for X, 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
ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) )
let X, 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 ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) ) )
assume ( 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 ) ; :: thesis: ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) )
then consider p being Element of P such that
A1: ( 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) ) ) ;
thus ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) ) by A1; :: thesis: verum