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;
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
A1: ex_sup_of (sup_op R) .: X,R and
A2: 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 A1; :: thesis: "\/" (((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; :: 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
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 c in X ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: verum