let R be upper-bounded Semilattice; :: thesis: for X being Subset of [:R,R:] st ex_inf_of (inf_op R) .: X,R holds
inf_op R preserves_inf_of X
set f = inf_op R;
let X be Subset of [:R,R:]; :: thesis: ( ex_inf_of (inf_op R) .: X,R implies inf_op R preserves_inf_of X )
assume that
A1: ex_inf_of (inf_op R) .: X,R and
A2: ex_inf_of X,[:R,R:] ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (inf_op R) .: X,R & "/\" (((inf_op R) .: X),R) = (inf_op R) . ("/\" (X,[:R,R:])) )
thus ex_inf_of (inf_op R) .: X,R by A1; :: thesis: "/\" (((inf_op R) .: X),R) = (inf_op R) . ("/\" (X,[:R,R:]))
A3: dom (inf_op R) = the carrier of [:R,R:] by FUNCT_2:def 1;
then A4: dom (inf_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 (inf_op R) .: X holds
(inf_op R) . (inf X) >= b

proof

let b be Element of R; :: thesis: ( b is_<=_than (inf_op R) .: X implies (inf_op R) . (inf X) >= b )
assume A6: b is_<=_than (inf_op R) .: X ; :: thesis: (inf_op R) . (inf X) >= b
X is_>=_than [b,b]

proof

let c be Element of [:R,R:]; :: according to LATTICE3:def 8 :: thesis: ( not c in X or [b,b] <= c )
assume c in X ; :: thesis: [b,b] <= c
then (inf_op R) . c in (inf_op R) .: X by A3, FUNCT_1:def 6;
then A7: b <= (inf_op R) . c 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: (inf_op R) . c = (inf_op R) . (s,t) by A9
.= s "/\" t by WAYBEL_2:def 4 ;
s "/\" t <= t by YELLOW_0:23;
then A11: b <= t by A7, A10, ORDERS_2:3;
s "/\" t <= s by YELLOW_0:23;
then b <= s by A7, A10, ORDERS_2:3;
hence [b,b] <= c by A9, A11, YELLOW_3:11; :: thesis: verum

end;

then [b,b] <= inf X by A2, YELLOW_0:def 10;
then (inf_op R) . (b,b) <= (inf_op R) . (inf X) by WAYBEL_1:def 2;
then b "/\" b <= (inf_op R) . (inf X) by WAYBEL_2:def 4;
hence b <= (inf_op R) . (inf X) by YELLOW_0:25; :: thesis: verum

end;

inf X is_<=_than X by A2, YELLOW_0:def 10;
then (inf_op R) . (inf X) is_<=_than (inf_op R) .: X by YELLOW_2:13;
hence "/\" (((inf_op R) .: X),R) = (inf_op R) . ("/\" (X,[:R,R:])) by A1, A5, YELLOW_0:def 10; :: thesis: verum