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 ; :: 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 9;
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 Def14;
A5: (Map2Rel L) . s in the carrier of (InclPoset (Aux L)) by A2, FUNCT_2:7;
A6: (Map2Rel L) . t in the carrier of (InclPoset (Aux L)) by A3, FUNCT_2:7;
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 by A7, Def9;
reconsider AS' = AS, AT' = AT as Element of by A2, A3, FUNCT_2:7;
for a, b being set st [a,b] in AS holds
[a,b] in AT

proof

let a, b be set ; :: 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:106;
reconsider a' = a, b' = b as Element of by A9, ZFMISC_1:106;
reconsider sb = s . b', tb = t . b' as Element of ;
ex a1, b1 being Element of st
( a1 = s . b & b1 = t . b & a1 <= b1 ) by A4, A10, YELLOW_2:def 1;
then A11: sb c= tb by YELLOW_1:3;
ex AR being auxiliary Relation of st
( AR = (Map2Rel L) . x & ( for a', b' being set holds
( [a',b'] in AR iff ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = a' & y' = b' & s' = x & x' in s' . y' ) ) ) ) by Def16;
then A12: ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = a' & y' = b' & s' = s & x' in s' . y' ) by A2, A9;
ex AR1 being auxiliary Relation of st
( AR1 = (Map2Rel L) . y & ( for a', b' being set holds
( [a',b'] in AR1 iff ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = a' & y' = b' & s' = y & x' in s' . y' ) ) ) ) by Def16;
hence [a,b] in AT by A3, A11, A12; :: thesis: verum

end;

then AS' c= AT' by RELAT_1:def 3;
then [AS',AT'] 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 9; :: thesis: verum