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