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