let P be non empty strict chain-complete Poset; :: thesis: for h being Function of (ConPoset P,P),P
for G being non empty Chain of (ConPoset P,P)
for x being set st x in G holds
h . x in h .: G
let h be Function of (ConPoset P,P),P; :: thesis: for G being non empty Chain of (ConPoset P,P)
for x being set st x in G holds
h . x in h .: G
let G be non empty Chain of (ConPoset P,P); :: thesis: for x being set st x in G holds
h . x in h .: G
let x be set ; :: thesis: ( x in G implies h . x in h .: G )
assume A1: x in G ; :: thesis: h . x in h .: G
set X = the carrier of (ConPoset P,P);
set Y = the carrier of P;
set y = h . x;
reconsider h = h as Function of the carrier of (ConPoset P,P),the carrier of P ;
x in the carrier of (ConPoset P,P) by A1;
then x in dom h by FUNCT_2:def 1;
hence h . x in h .: G by A1, FUNCT_1:def 12; :: thesis: verum