let L be lower-bounded sup-Semilattice; :: thesis: Map2Rel L is monotone
set f = Map2Rel L;
A1: InclPoset (Aux L) = RelStr(# (Aux L),(RelIncl (Aux L)) #) by YELLOW_1:def 1;
let x, y be Element of (MonSet L); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of (InclPoset (Aux L)) holds
( not b₁ = (Map2Rel L) . x or not b₂ = (Map2Rel L) . y or b₁ <= b₂ ) )
assume x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of (InclPoset (Aux L)) holds
( not b₁ = (Map2Rel L) . x or not b₂ = (Map2Rel L) . y or b₁ <= b₂ )
then [x,y] in the InternalRel of (MonSet L) by ORDERS_2:def 5;
then consider s, t being Function of L,(InclPoset (Ids L)) such that
A2: x = s and
A3: y = t and
x in the carrier of (MonSet L) and
y in the carrier of (MonSet L) and
A4: s <= t by Def13;
A5: (Map2Rel L) . s in the carrier of (InclPoset (Aux L)) by A2, FUNCT_2:5;
A6: (Map2Rel L) . t in the carrier of (InclPoset (Aux L)) by A3, FUNCT_2:5;
A7: (Map2Rel L) . s in Aux L by A5, YELLOW_1:1;
A8: (Map2Rel L) . t in Aux L by A6, YELLOW_1:1;
then reconsider AS = (Map2Rel L) . s, AT = (Map2Rel L) . t as auxiliary Relation of L by A7, Def8;
reconsider AS9 = AS, AT9 = AT as Element of (InclPoset (Aux L)) by A2, A3, FUNCT_2:5;
for a, b being object st [a,b] in AS holds
[a,b] in AT

proof

let a, b be object ; :: thesis: ( [a,b] in AS implies [a,b] in AT )
assume A9: [a,b] in AS ; :: thesis: [a,b] in AT
then A10: b in the carrier of L by ZFMISC_1:87;
reconsider a9 = a, b9 = b as Element of L by A9, ZFMISC_1:87;
reconsider sb = s . b9, tb = t . b9 as Element of (InclPoset (Ids L)) ;
ex a1, b1 being Element of (InclPoset (Ids L)) st
( a1 = s . b & b1 = t . b & a1 <= b1 ) by A4, A10;
then A11: sb c= tb by YELLOW_1:3;
ex AR being auxiliary Relation of L st
( AR = (Map2Rel L) . x & ( for a9, b9 being object holds
( [a9,b9] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = a9 & y9 = b9 & s9 = x & x9 in s9 . y9 ) ) ) ) by Def15;
then A12: ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = a9 & y9 = b9 & s9 = s & x9 in s9 . y9 ) by A2, A9;
ex AR1 being auxiliary Relation of L st
( AR1 = (Map2Rel L) . y & ( for a9, b9 being object holds
( [a9,b9] in AR1 iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = a9 & y9 = b9 & s9 = y & x9 in s9 . y9 ) ) ) ) by Def15;
hence [a,b] in AT by A3, A11, A12; :: thesis: verum

end;

then AS9 c= AT9 by RELAT_1:def 3;
then [AS9,AT9] in RelIncl (Aux L) by A7, A8, WELLORD2:def 1;
hence for b₁, b₂ being Element of the carrier of (InclPoset (Aux L)) holds
( not b₁ = (Map2Rel L) . x or not b₂ = (Map2Rel L) . y or b₁ <= b₂ ) by A1, A2, A3, ORDERS_2:def 5; :: thesis: verum