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 set 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 set ; :: 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 B1: ( 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 set such that
B2: ( a in dom h & a in K & x = h . a ) by B1, FUNCT_1:def 12;
consider b being set such that
B3: ( b in dom h & b in K & y = h . b ) by B1, FUNCT_1:def 12;
reconsider a = a, b = b as Element of P1 by B2, B3;
( a <= b or b <= a ) by ORDERS_2:38, B2, B3;
then ( x <= y or y <= x ) by ORDERS_3:def 5, B2, B3;
hence ( [x,y] in the InternalRel of P2 or [y,x] in the InternalRel of P2 ) by ORDERS_2:def 9; :: thesis: verum

end;

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

proof

let x be set ; :: 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 9; :: 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 A1, ORDERS_1:92;
then reconsider K2 = h .: K as Chain of P2 by ORDERS_2:def 11;
consider a being set such that
A2: a in K by XBOOLE_0:7;
a in the carrier of P1 by A2;
then a in dom h by FUNCT_2:def 1;
then h . a in K2 by FUNCT_1:def 12, A2;
hence h .: K is non empty Chain of P2 ; :: thesis: verum