let P1, P2 be non empty Poset; :: thesis: for K being non empty Chain of P1
for h being monotone Function of P1,P2 holds h .: K is non empty Chain of P2
let K be non empty Chain of P1; :: thesis: for h being monotone Function of P1,P2 holds h .: K is non empty Chain of P2
let h be monotone Function of P1,P2; :: thesis: h .: K is non empty Chain of P2
set R = the InternalRel of P2;
set K2 = h .: K;
for x, y being object st x in h .: K & y in h .: K & x <> y & not [x,y] in the InternalRel of P2 holds
[y,x] in the InternalRel of P2

proof

let x, y be object ; :: thesis: ( x in h .: K & y in h .: K & x <> y & not [x,y] in the InternalRel of P2 implies [y,x] in the InternalRel of P2 )
assume A1: ( x in h .: K & y in h .: K & x <> y ) ; :: thesis: ( [x,y] in the InternalRel of P2 or [y,x] in the InternalRel of P2 )
then reconsider x = x, y = y as Element of P2 ;
consider a being object such that
A2: ( a in dom h & a in K & x = h . a ) by A1, FUNCT_1:def 6;
consider b being object such that
A3: ( b in dom h & b in K & y = h . b ) by A1, FUNCT_1:def 6;
reconsider a = a, b = b as Element of P1 by A2, A3;
( a <= b or b <= a ) by A2, A3, ORDERS_2:11;
then ( x <= y or y <= x ) by A2, A3, ORDERS_3:def 5;
hence ( [x,y] in the InternalRel of P2 or [y,x] in the InternalRel of P2 ) by ORDERS_2:def 5; :: thesis: verum

end;

then A4: the InternalRel of P2 is_connected_in h .: K by RELAT_2:def 6;
for x being object st x in h .: K holds
[x,x] in the InternalRel of P2

proof

let x be object ; :: thesis: ( x in h .: K implies [x,x] in the InternalRel of P2 )
assume x in h .: K ; :: thesis: [x,x] in the InternalRel of P2
then reconsider x = x as Element of P2 ;
x <= x ;
hence [x,x] in the InternalRel of P2 by ORDERS_2:def 5; :: thesis: verum

end;

then the InternalRel of P2 is_reflexive_in h .: K by RELAT_2:def 1;
then the InternalRel of P2 is_strongly_connected_in h .: K by A4, ORDERS_1:7;
then reconsider K2 = h .: K as Chain of P2 by ORDERS_2:def 7;
consider a being object such that
A5: a in K by XBOOLE_0:7;
a in the carrier of P1 by A5;
then a in dom h by FUNCT_2:def 1;
then h . a in K2 by A5, FUNCT_1:def 6;
hence h .: K is non empty Chain of P2 ; :: thesis: verum