let L be lower-bounded sup-Semilattice; :: thesis:
set J = the carrier of L --> (InclPoset (Ids L));
A1: the carrier of (MonSet L) c= the carrier of ((InclPoset (Ids L)) |^ the carrier of L)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in the carrier of (MonSet L) ; :: thesis:
then consider s being Function of L,(InclPoset (Ids L)) such that
A2: a = s and
s is monotone and
for x being Element of L holds s . x c= downarrow x by Def13;
s in Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) by FUNCT_2:8;
hence a in the carrier of ((InclPoset (Ids L)) |^ the carrier of L) by A2, YELLOW_1:28; :: thesis:

end;

A3: the InternalRel of (MonSet L) c= the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L)

proof

let a, b be object ; :: according to RELAT_1:def 3 :: thesis:
assume [a,b] in the InternalRel of (MonSet L) ; :: thesis:
then consider f, g being Function of L,(InclPoset (Ids L)) such that
A4: a = f and
A5: b = g and
a in the carrier of (MonSet L) and
b in the carrier of (MonSet L) and
A6: f <= g by Def13;
set AG = product ( the carrier of L --> (InclPoset (Ids L)));
A7: product ( the carrier of L --> (InclPoset (Ids L))) = (InclPoset (Ids L)) |^ the carrier of L by YELLOW_1:def 5;
A8: f in Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) by FUNCT_2:8;
A9: g in Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) by FUNCT_2:8;
A10: f in the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))) by A7, A8, YELLOW_1:28;
reconsider f9 = f, g9 = g as Element of (product ( the carrier of L --> (InclPoset (Ids L)))) by A7, A8, A9, YELLOW_1:28;
A11: f9 in product (Carrier ( the carrier of L --> (InclPoset (Ids L)))) by A10, YELLOW_1:def 4;
ex ff, gg being Function st
( ff = f9 & gg = g9 & ( for i being object st i in the carrier of L holds
ex R being RelStr ex xi, yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = ff . i & yi = gg . i & xi <= yi ) ) )

proof

take f ; :: thesis:
take g ; :: thesis:
thus ( f = f9 & g = g9 ) ; :: thesis:
let i be object ; :: thesis:
assume A12: i in the carrier of L ; :: thesis:
then reconsider i9 = i as Element of L ;
take R = InclPoset (Ids L); :: thesis:
reconsider xi = f . i9, yi = g . i9 as Element of R ;
take xi ; :: thesis:
take yi ; :: thesis:
thus ( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = f . i & yi = g . i ) by A12, FUNCOP_1:7; :: thesis:
reconsider i9 = i as Element of L by A12;
ex a, b being Element of (InclPoset (Ids L)) st
( a = f . i9 & b = g . i9 & a <= b ) by A6;
hence xi <= yi ; :: thesis:

end;

then f9 <= g9 by A11, YELLOW_1:def 4;
then [a,b] in the InternalRel of (product ( the carrier of L --> (InclPoset (Ids L)))) by A4, A5, ORDERS_2:def 5;
hence [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) by YELLOW_1:def 5; :: thesis:

end;

set J = the carrier of L --> (InclPoset (Ids L));
the InternalRel of (MonSet L) = the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) |_2 the carrier of (MonSet L)

proof

let a, b be object ; :: according to RELAT_1:def 2 :: thesis:
thus ( [a,b] in the InternalRel of (MonSet L) implies [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) |_2 the carrier of (MonSet L) ) by A3, XBOOLE_0:def 4; :: thesis:
assume A13: [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) |_2 the carrier of (MonSet L) ; :: thesis:
then A14: [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) by XBOOLE_0:def 4;
A15: [a,b] in [: the carrier of (MonSet L), the carrier of (MonSet L):] by A13, XBOOLE_0:def 4;
A16: a in the carrier of ((InclPoset (Ids L)) |^ the carrier of L) by A14, ZFMISC_1:87;
A17: b in the carrier of ((InclPoset (Ids L)) |^ the carrier of L) by A14, ZFMISC_1:87;
A18: a in the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))) by A16, YELLOW_1:def 5;
reconsider a9 = a, b9 = b as Element of (product ( the carrier of L --> (InclPoset (Ids L)))) by A16, A17, YELLOW_1:def 5;
[a9,b9] in the InternalRel of (product ( the carrier of L --> (InclPoset (Ids L)))) by A14, YELLOW_1:def 5;
then A19: a9 <= b9 by ORDERS_2:def 5;
a9 in product (Carrier ( the carrier of L --> (InclPoset (Ids L)))) by A18, YELLOW_1:def 4;
then consider f, g being Function such that
A20: f = a9 and
A21: g = b9 and
A22: for i being object st i in the carrier of L holds
ex R being RelStr ex xi, yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . i & xi = f . i & yi = g . i & xi <= yi ) by A19, YELLOW_1:def 4;
A23: f in Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) by A16, A20, YELLOW_1:28;
g in Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) by A17, A21, YELLOW_1:28;
then reconsider f = f, g = g as Function of the carrier of L, the carrier of (InclPoset (Ids L)) by A23, FUNCT_2:66;
reconsider f = f, g = g as Function of L,(InclPoset (Ids L)) ;

now :: thesis:

take f = f; :: thesis:
take g = g; :: thesis:
f <= g

proof

let j be set ; :: according to YELLOW_2:def 1 :: thesis:
assume j in the carrier of L ; :: thesis:
then reconsider j9 = j as Element of L ;
take f . j9 ; :: thesis:
take g . j9 ; :: thesis:
ex R being RelStr ex xi, yi being Element of R st
( R = ( the carrier of L --> (InclPoset (Ids L))) . j9 & xi = f . j9 & yi = g . j9 & xi <= yi ) by A22;
hence ( f . j9 = f . j & g . j9 = g . j & f . j9 <= g . j9 ) ; :: thesis:

end;

hence ( a9 = f & b9 = g & a9 in the carrier of (MonSet L) & b9 in the carrier of (MonSet L) & f <= g ) by A15, A20, A21, ZFMISC_1:87; :: thesis:

end;

hence [a,b] in the InternalRel of (MonSet L) by Def13; :: thesis:

end;

hence MonSet L is full SubRelStr of (InclPoset (Ids L)) |^ the carrier of L by A1, A3, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis: