let R be upper-bounded Semilattice; 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:]; ( 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:]
; WAYBEL_0:def 30 ( 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; "/\" (((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;
( b is_<=_than (inf_op R) .: X implies (inf_op R) . (inf X) >= b )
assume A6:
b is_<=_than (inf_op R) .: X
;
(inf_op R) . (inf X) >= b
X is_>=_than [b,b]
proof
let c be
Element of
[:R,R:];
LATTICE3:def 8 ( not c in X or [b,b] <= c )
assume
c in X
;
[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;
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;
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; verum