let L be lower-bounded sup-Semilattice; 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); ORDERS_3:def 5 ( 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
; 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 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 ;
( [a,b] in AS implies [a,b] in AT )
assume A9:
[a,b] in AS
;
[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;
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 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, A3, ORDERS_2:def 5; verum