let P1, P2 be non empty Poset; 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; 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; 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 ;
( 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 )
;
( [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;
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
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
; verum