let L be lower-bounded LATTICE; for R being auxiliary Relation of L holds
( R is multiplicative iff R -below is meet-preserving )
let R be auxiliary Relation of L; ( R is multiplicative iff R -below is meet-preserving )
hereby ( R -below is meet-preserving implies R is multiplicative )
assume A1:
R is
multiplicative
;
R -below is meet-preserving thus
R -below is
meet-preserving
verumproof
let x,
y be
Element of
L;
WAYBEL_0:def 34 R -below preserves_inf_of {x,y}
A2:
(R -below) . y = R -below y
by WAYBEL_4:def 12;
A3:
R -below (x "/\" y) = (R -below x) /\ (R -below y)
proof
hereby TARSKI:def 3,
XBOOLE_0:def 10 (R -below x) /\ (R -below y) c= R -below (x "/\" y)
let a be
object ;
( a in R -below (x "/\" y) implies a in (R -below x) /\ (R -below y) )assume
a in R -below (x "/\" y)
;
a in (R -below x) /\ (R -below y)then
a in { z where z is Element of L : [z,(x "/\" y)] in R }
by WAYBEL_4:def 10;
then consider z being
Element of
L such that A4:
a = z
and A5:
[z,(x "/\" y)] in R
;
A6:
z <= z
;
x "/\" y <= y
by YELLOW_0:23;
then
[z,y] in R
by A5, A6, WAYBEL_4:def 4;
then A7:
z in R -below y
by WAYBEL_4:13;
x "/\" y <= x
by YELLOW_0:23;
then
[z,x] in R
by A5, A6, WAYBEL_4:def 4;
then
z in R -below x
by WAYBEL_4:13;
hence
a in (R -below x) /\ (R -below y)
by A4, A7, XBOOLE_0:def 4;
verum
end;
let a be
object ;
TARSKI:def 3 ( not a in (R -below x) /\ (R -below y) or a in R -below (x "/\" y) )
assume A8:
a in (R -below x) /\ (R -below y)
;
a in R -below (x "/\" y)
then reconsider z =
a as
Element of
L ;
a in R -below y
by A8, XBOOLE_0:def 4;
then A9:
[z,y] in R
by WAYBEL_4:13;
a in R -below x
by A8, XBOOLE_0:def 4;
then
[z,x] in R
by WAYBEL_4:13;
then
[z,(x "/\" y)] in R
by A1, A9;
hence
a in R -below (x "/\" y)
by WAYBEL_4:13;
verum
end;
(
(R -below) . (x "/\" y) = R -below (x "/\" y) &
(R -below) . x = R -below x )
by WAYBEL_4:def 12;
then
(R -below) . (x "/\" y) = ((R -below) . x) "/\" ((R -below) . y)
by A2, A3, YELLOW_2:43;
hence
R -below preserves_inf_of {x,y}
by YELLOW_3:8;
verum
end;
end;
assume A10:
for x, y being Element of L holds R -below preserves_inf_of {x,y}
; WAYBEL_0:def 34 R is multiplicative
let a, x, y be Element of L; WAYBEL_7:def 7 ( [a,x] in R & [a,y] in R implies [a,(x "/\" y)] in R )
R -below preserves_inf_of {x,y}
by A10;
then A11: (R -below) . (x "/\" y) =
((R -below) . x) "/\" ((R -below) . y)
by YELLOW_3:8
.=
((R -below) . x) /\ ((R -below) . y)
by YELLOW_2:43
;
A12:
(R -below) . y = R -below y
by WAYBEL_4:def 12;
assume
( [a,x] in R & [a,y] in R )
; [a,(x "/\" y)] in R
then A13:
( a in R -below x & a in R -below y )
by WAYBEL_4:13;
( (R -below) . (x "/\" y) = R -below (x "/\" y) & (R -below) . x = R -below x )
by WAYBEL_4:def 12;
then
a in R -below (x "/\" y)
by A11, A12, A13, XBOOLE_0:def 4;
hence
[a,(x "/\" y)] in R
by WAYBEL_4:13; verum