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