let L be lower-bounded LATTICE; :: thesis: 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; :: thesis: ( 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 :: thesis: ( ( 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 ; :: thesis: 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 a, b, x, y be Element of L; :: thesis: ( [a,x] in R & [b,y] in R implies [(a "/\" b),(x "/\" y)] in R )
assume A2: ( [a,x] in R & [b,y] in R ) ; :: thesis: [(a "/\" b),(x "/\" y)] in R
( a >= a "/\" b & a "/\" b <= b & x <= x & y <= y ) by YELLOW_0:23;
then ( [(a "/\" b),x] in R & [(a "/\" b),y] in R ) by A2, WAYBEL_4:def 5;
hence [(a "/\" b),(x "/\" y)] in R by A1, Def7; :: thesis: verum

end;

assume A3: 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 ; :: thesis: R is multiplicative
let a be Element of L; :: according to WAYBEL_7:def 7 :: thesis: 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 A3; :: thesis: verum