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;
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 6; :: thesis: verum