let R be lower-bounded sup-Semilattice; for X being Subset of [:R,R:] st ex_sup_of (sup_op R) .: X,R holds
sup_op R preserves_sup_of X
set f = sup_op R;
let X be Subset of [:R,R:]; ( ex_sup_of (sup_op R) .: X,R implies sup_op R preserves_sup_of X )
assume that
A1:
ex_sup_of (sup_op R) .: X,R
and
A2:
ex_sup_of X,[:R,R:]
; WAYBEL_0:def 31 ( ex_sup_of (sup_op R) .: X,R & "\/" (((sup_op R) .: X),R) = (sup_op R) . ("\/" (X,[:R,R:])) )
thus
ex_sup_of (sup_op R) .: X,R
by A1; "\/" (((sup_op R) .: X),R) = (sup_op R) . ("\/" (X,[:R,R:]))
A3:
dom (sup_op R) = the carrier of [:R,R:]
by FUNCT_2:def 1;
then A4:
dom (sup_op R) = [: the carrier of R, the carrier of R:]
by YELLOW_3:def 2;
A5:
for b being Element of R st b is_>=_than (sup_op R) .: X holds
(sup_op R) . (sup X) <= b
proof
let b be
Element of
R;
( b is_>=_than (sup_op R) .: X implies (sup_op R) . (sup X) <= b )
assume A6:
b is_>=_than (sup_op R) .: X
;
(sup_op R) . (sup X) <= b
X is_<=_than [b,b]
proof
let c be
Element of
[:R,R:];
LATTICE3:def 9 ( not c in X or c <= [b,b] )
assume
c in X
;
c <= [b,b]
then
(sup_op R) . c in (sup_op R) .: X
by A3, FUNCT_1:def 6;
then A7:
(sup_op R) . c <= b
by A6;
consider s,
t being
object such that A8:
(
s in the
carrier of
R &
t in the
carrier of
R )
and A9:
c = [s,t]
by A3, A4, ZFMISC_1:def 2;
reconsider s =
s,
t =
t as
Element of
R by A8;
A10:
(sup_op R) . c =
(sup_op R) . (
s,
t)
by A9
.=
s "\/" t
by WAYBEL_2:def 5
;
t <= s "\/" t
by YELLOW_0:22;
then A11:
t <= b
by A7, A10, ORDERS_2:3;
s <= s "\/" t
by YELLOW_0:22;
then
s <= b
by A7, A10, ORDERS_2:3;
hence
c <= [b,b]
by A9, A11, YELLOW_3:11;
verum
end;
then
sup X <= [b,b]
by A2, YELLOW_0:def 9;
then
(sup_op R) . (sup X) <= (sup_op R) . (
b,
b)
by WAYBEL_1:def 2;
then
(
b <= b &
(sup_op R) . (sup X) <= b "\/" b )
by WAYBEL_2:def 5;
hence
(sup_op R) . (sup X) <= b
by YELLOW_0:24;
verum
end;
X is_<=_than sup X
by A2, YELLOW_0:def 9;
then
(sup_op R) .: X is_<=_than (sup_op R) . (sup X)
by YELLOW_2:14;
hence
"\/" (((sup_op R) .: X),R) = (sup_op R) . ("\/" (X,[:R,R:]))
by A1, A5, YELLOW_0:def 9; verum