let L be lower-bounded LATTICE; for R being auxiliary Relation of L holds
( R is multiplicative iff for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds
[(a "/\" b),(x "/\" y)] in R )
let R be auxiliary Relation of L; ( R is multiplicative iff for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds
[(a "/\" b),(x "/\" y)] in R )
hereby ( ( for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds
[(a "/\" b),(x "/\" y)] in R ) implies R is multiplicative )
assume A1:
R is
multiplicative
;
for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds
[(a "/\" b),(x "/\" y)] in Rlet a,
b,
x,
y be
Element of
L;
( [a,x] in R & [b,y] in R implies [(a "/\" b),(x "/\" y)] in R )assume that A2:
[a,x] in R
and A3:
[b,y] in R
;
[(a "/\" b),(x "/\" y)] in R
(
a "/\" b <= b &
y <= y )
by YELLOW_0:23;
then A4:
[(a "/\" b),y] in R
by A3, WAYBEL_4:def 4;
(
a >= a "/\" b &
x <= x )
by YELLOW_0:23;
then
[(a "/\" b),x] in R
by A2, WAYBEL_4:def 4;
hence
[(a "/\" b),(x "/\" y)] in R
by A1, A4;
verum
end;
assume A5:
for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds
[(a "/\" b),(x "/\" y)] in R
; R is multiplicative
let a be Element of L; WAYBEL_7:def 7 for x, y being Element of L st [a,x] in R & [a,y] in R holds
[a,(x "/\" y)] in R
a "/\" a = a
by YELLOW_0:25;
hence
for x, y being Element of L st [a,x] in R & [a,y] in R holds
[a,(x "/\" y)] in R
by A5; verum