let L be lower-bounded sup-Semilattice; :: thesis: Rel2Map L is monotone
let x, y be Element of (InclPoset (Aux L)); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b1, b2 being Element of the carrier of (MonSet L) holds
( not b1 = (Rel2Map L) . x or not b2 = (Rel2Map L) . y or b1 <= b2 ) )
( x in the carrier of (InclPoset (Aux L)) & y in the carrier of (InclPoset (Aux L)) )
;
then
( x in Aux L & y in Aux L )
by YELLOW_1:1;
then reconsider R1 = x, R2 = y as auxiliary Relation of L by Def9;
assume
x <= y
; :: thesis: for b1, b2 being Element of the carrier of (MonSet L) holds
( not b1 = (Rel2Map L) . x or not b2 = (Rel2Map L) . y or b1 <= b2 )
then A1:
x c= y
by YELLOW_1:3;
let a, b be Element of (MonSet L); :: thesis: ( not a = (Rel2Map L) . x or not b = (Rel2Map L) . y or a <= b )
assume A2:
( a = (Rel2Map L) . x & b = (Rel2Map L) . y )
; :: thesis: a <= b
thus
a <= b
:: thesis: verumproof
A3:
(
(Rel2Map L) . x = R1 -below &
(Rel2Map L) . y = R2 -below )
by Def15;
consider s being
Function of
L,
(InclPoset (Ids L)) such that A4:
(
(Rel2Map L) . x = s &
s is
monotone & ( for
x being
Element of
L holds
s . x c= downarrow x ) )
by Def14;
consider t being
Function of
L,
(InclPoset (Ids L)) such that A5:
(
(Rel2Map L) . y = t &
t is
monotone & ( for
x being
Element of
L holds
t . x c= downarrow x ) )
by Def14;
s <= t
proof
let q be
set ;
:: according to YELLOW_2:def 1 :: thesis: ( not q in the carrier of L or ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = s . q & b2 = t . q & b1 <= b2 ) )
assume
q in the
carrier of
L
;
:: thesis: ex b1, b2 being Element of the carrier of (InclPoset (Ids L)) st
( b1 = s . q & b2 = t . q & b1 <= b2 )
then reconsider q' =
q as
Element of
L ;
A6:
s . q = R1 -below q'
by A3, A4, Def13;
A7:
t . q = R2 -below q'
by A3, A5, Def13;
A8:
R1 -below q' c= R2 -below q'
by A1, Th29;
reconsider sq =
s . q',
tq =
t . q' as
Element of
(InclPoset (Ids L)) ;
sq <= tq
by A6, A7, A8, YELLOW_1:3;
hence
ex
b1,
b2 being
Element of the
carrier of
(InclPoset (Ids L)) st
(
b1 = s . q &
b2 = t . q &
b1 <= b2 )
;
:: thesis: verum
end;
then
[(R1 -below ),(R2 -below )] in the
InternalRel of
(MonSet L)
by A3, A4, A5, Def14;
hence
a <= b
by A2, A3, ORDERS_2:def 9;
:: thesis: verum
end;