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 set ; :: 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 & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) by Def14;
s in Funcs the carrier of L,the carrier of (InclPoset (Ids L)) by FUNCT_2:11;
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 set ; :: 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 & b = g & a in the carrier of (MonSet L) & b in the carrier of (MonSet L) & f <= g ) by Def14;
set AG = product (the carrier of L --> (InclPoset (Ids L)));
A5: product (the carrier of L --> (InclPoset (Ids L))) = (InclPoset (Ids L)) |^ the carrier of L by YELLOW_1:def 5;
A6: ( f in Funcs the carrier of L,the carrier of (InclPoset (Ids L)) & g in Funcs the carrier of L,the carrier of (InclPoset (Ids L)) ) by FUNCT_2:11;
then A7: ( f in the carrier of (product (the carrier of L --> (InclPoset (Ids L)))) & g in the carrier of (product (the carrier of L --> (InclPoset (Ids L)))) ) by A5, YELLOW_1:28;
reconsider f' = f, g' = g as Element of (product (the carrier of L --> (InclPoset (Ids L)))) by A5, A6, YELLOW_1:28;
A8: f' in product (Carrier (the carrier of L --> (InclPoset (Ids L)))) by A7, YELLOW_1:def 4;
ex ff, gg being Function st
( ff = f' & gg = g' & ( for i being set 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 = f' & g = g' ) ; :: thesis:
let i be set ; :: thesis:
assume A9: i in the carrier of L ; :: thesis:
then reconsider i' = i as Element of L ;
take R = InclPoset (Ids L); :: thesis:
reconsider xi = f . i', yi = g . i' 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 A9, FUNCOP_1:13; :: thesis:
reconsider i' = i as Element of L by A9;
consider a, b being Element of (InclPoset (Ids L)) such that
A10: ( a = f . i' & b = g . i' & a <= b ) by A4, YELLOW_2:def 1;
thus xi <= yi by A10; :: thesis:

end;

then f' <= g' by A8, YELLOW_1:def 4;
then [a,b] in the InternalRel of (product (the carrier of L --> (InclPoset (Ids L)))) by A4, ORDERS_2:def 9;
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 set ; :: 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 [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) |_2 the carrier of (MonSet L) ; :: thesis:
then A11: ( [a,b] in the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) & [a,b] in [:the carrier of (MonSet L),the carrier of (MonSet L):] ) by XBOOLE_0:def 4;
then A12: ( a in the carrier of ((InclPoset (Ids L)) |^ the carrier of L) & b in the carrier of ((InclPoset (Ids L)) |^ the carrier of L) ) by ZFMISC_1:106;
then A13: ( a in the carrier of (product (the carrier of L --> (InclPoset (Ids L)))) & b in the carrier of (product (the carrier of L --> (InclPoset (Ids L)))) ) by YELLOW_1:def 5;
reconsider a' = a, b' = b as Element of (product (the carrier of L --> (InclPoset (Ids L)))) by A12, YELLOW_1:def 5;
[a',b'] in the InternalRel of (product (the carrier of L --> (InclPoset (Ids L)))) by A11, YELLOW_1:def 5;
then A14: a' <= b' by ORDERS_2:def 9;
a' in product (Carrier (the carrier of L --> (InclPoset (Ids L)))) by A13, YELLOW_1:def 4;
then consider f, g being Function such that
A15: ( f = a' & g = b' & ( for i being set 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 A14, YELLOW_1:def 4;
( f in Funcs the carrier of L,the carrier of (InclPoset (Ids L)) & g in Funcs the carrier of L,the carrier of (InclPoset (Ids L)) ) by A12, A15, YELLOW_1:28;
then reconsider f = f, g = g as Function of the carrier of L,the carrier of (InclPoset (Ids L)) by FUNCT_2:121;
reconsider f = f, g = g as Function of L,(InclPoset (Ids L)) ;

now

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 j' = j as Element of L ;
take f . j' ; :: thesis:
take g . j' ; :: thesis:
consider R being RelStr , xi, yi being Element of R such that
A16: ( R = (the carrier of L --> (InclPoset (Ids L))) . j' & xi = f . j' & yi = g . j' & xi <= yi ) by A15;
thus ( f . j' = f . j & g . j' = g . j & f . j' <= g . j' ) by A16, FUNCOP_1:13; :: thesis:

end;

hence ( a' = f & b' = g & a' in the carrier of (MonSet L) & b' in the carrier of (MonSet L) & f <= g ) by A11, A15, ZFMISC_1:106; :: thesis:

end;

hence [a,b] in the InternalRel of (MonSet L) by Def14; :: 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: