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;
A1:
dom (inf_op R) = the carrier of [:R,R:]
by FUNCT_2:def 1;
then A2:
dom (inf_op R) = [:the carrier of R,the carrier of R:]
by YELLOW_3:def 2;
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
A3:
ex_inf_of (inf_op R) .: X,R
and
A4:
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 A3; :: thesis: "/\" ((inf_op R) .: X),R = (inf_op R) . ("/\" X,[:R,R:])
inf X is_<=_than X
by A4, YELLOW_0:def 10;
then A5:
(inf_op R) . (inf X) is_<=_than (inf_op R) .: X
by YELLOW_2:15;
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 A7:
c in X
;
:: thesis: [b,b] <= c
consider s,
t being
set such that A8:
(
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 A8;
(inf_op R) . c in (inf_op R) .: X
by A1, A7, FUNCT_1:def 12;
then A9:
b <= (inf_op R) . c
by A6, LATTICE3:def 8;
A10:
(inf_op R) . c =
(inf_op R) . s,
t
by A8
.=
s "/\" t
by WAYBEL_2:def 4
;
(
s "/\" t <= s &
s "/\" t <= t )
by YELLOW_0:23;
then
(
b <= s &
b <= t )
by A9, A10, ORDERS_2:26;
hence
[b,b] <= c
by A8, YELLOW_3:11;
:: thesis: verum
end;
then
[b,b] <= inf X
by A4, 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;
hence
"/\" ((inf_op R) .: X),R = (inf_op R) . ("/\" X,[:R,R:])
by A3, A5, YELLOW_0:def 10; :: thesis: verum