let L be lower-bounded LATTICE; :: thesis: for R being auxiliary Relation of L holds
( R is multiplicative iff R -below is meet-preserving )
let R be auxiliary Relation of L; :: thesis: ( R is multiplicative iff R -below is meet-preserving )

hereby :: thesis: ( R -below is meet-preserving implies R is multiplicative )

assume A1: R is multiplicative ; :: thesis: R -below is meet-preserving
thus R -below is meet-preserving :: thesis: verum

proof

let x, y be Element of L; :: according to WAYBEL_0:def 34 :: thesis: 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 :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (R -below x) /\ (R -below y) c= R -below (x "/\" y)

let a be object ; :: thesis: ( a in R -below (x "/\" y) implies a in (R -below x) /\ (R -below y) )
assume a in R -below (x "/\" y) ; :: thesis: 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; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

end;

assume A10: for x, y being Element of L holds R -below preserves_inf_of {x,y} ; :: according to WAYBEL_0:def 34 :: thesis: R is multiplicative
let a, x, y be Element of L; :: according to WAYBEL_7:def 7 :: thesis: ( [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 ) ; :: thesis: [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; :: thesis: verum