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 b1, b2 being Element of the carrier of (InclPoset (Aux L)) holds
( not b1 = (Map2Rel L) . x or not b2 = (Map2Rel L) . y or b1 <= b2 ) )
assume
x <= y
; :: thesis: for b1, b2 being Element of the carrier of (InclPoset (Aux L)) holds
( not b1 = (Map2Rel L) . x or not b2 = (Map2Rel L) . y or b1 <= b2 )
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 & y = t & x in the carrier of (MonSet L) & y in the carrier of (MonSet L) & s <= t )
by Def14;
( (Map2Rel L) . s in the carrier of (InclPoset (Aux L)) & (Map2Rel L) . t in the carrier of (InclPoset (Aux L)) )
by A2, FUNCT_2:7;
then A3:
( (Map2Rel L) . s in Aux L & (Map2Rel L) . t in Aux L )
by YELLOW_1:1;
then reconsider AS = (Map2Rel L) . s, AT = (Map2Rel L) . t as auxiliary Relation of L by Def9;
reconsider AS' = AS, AT' = AT as Element of (InclPoset (Aux L)) by A2, FUNCT_2:7;
AS' c= AT'
proof
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 A4:
[a,b] in AS
;
:: thesis: [a,b] in AT
then A5:
(
a in the
carrier of
L &
b in the
carrier of
L )
by ZFMISC_1:106;
reconsider a' =
a,
b' =
b as
Element of
L by A4, ZFMISC_1:106;
reconsider sb =
s . b',
tb =
t . b' as
Element of
(InclPoset (Ids L)) ;
consider a1,
b1 being
Element of
(InclPoset (Ids L)) such that A6:
(
a1 = s . b &
b1 = t . b &
a1 <= b1 )
by A2, A5, YELLOW_2:def 1;
A7:
sb c= tb
by A6, YELLOW_1:3;
consider AR being
auxiliary Relation of
L such that A8:
(
AR = (Map2Rel L) . x & ( for
a',
b' being
set holds
(
[a',b'] in AR iff ex
x',
y' being
Element of
L ex
s' being
Function of
L,
(InclPoset (Ids L)) st
(
x' = a' &
y' = b' &
s' = x &
x' in s' . y' ) ) ) )
by Def16;
consider x',
y' being
Element of
L,
s' being
Function of
L,
(InclPoset (Ids L)) such that A9:
(
x' = a' &
y' = b' &
s' = s &
x' in s' . y' )
by A2, A4, A8;
consider AR1 being
auxiliary Relation of
L such that A10:
(
AR1 = (Map2Rel L) . y & ( for
a',
b' being
set holds
(
[a',b'] in AR1 iff ex
x',
y' being
Element of
L ex
s' being
Function of
L,
(InclPoset (Ids L)) st
(
x' = a' &
y' = b' &
s' = y &
x' in s' . y' ) ) ) )
by Def16;
thus
[a,b] in AT
by A2, A7, A9, A10;
:: thesis: verum
end;
hence
AS' c= AT'
by RELAT_1:def 3;
:: thesis: verum
end;
then
[AS',AT'] in RelIncl (Aux L)
by A3, WELLORD2:def 1;
hence
for b1, b2 being Element of the carrier of (InclPoset (Aux L)) holds
( not b1 = (Map2Rel L) . x or not b2 = (Map2Rel L) . y or b1 <= b2 )
by A1, A2, ORDERS_2:def 9; :: thesis: verum