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 ) . (x "/\" y) = R -below (x "/\" y) & (R -below ) . x = R -below x & (R -below ) . y = R -below y ) by WAYBEL_4:def 13;
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 set ; :: 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 11;
then consider z being Element of L such that
A3: ( a = z & [z,(x "/\" y)] in R ) ;
( x "/\" y <= x & x "/\" y <= y & z <= z ) by YELLOW_0:23;
then ( [z,x] in R & [z,y] in R ) by A3, WAYBEL_4:def 5;
then ( z in R -below x & z in R -below y ) by WAYBEL_4:13;
hence a in (R -below x) /\ (R -below y) by A3, XBOOLE_0:def 4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (R -below x) /\ (R -below y) or a in R -below (x "/\" y) )
assume A4: a in (R -below x) /\ (R -below y) ; :: thesis: a in R -below (x "/\" y)
then A5: ( a in R -below x & a in R -below y ) by XBOOLE_0:def 4;
reconsider z = a as Element of L by A4;
( [z,x] in R & [z,y] in R ) by A5, WAYBEL_4:13;
then [z,(x "/\" y)] in R by A1, Def7;
hence a in R -below (x "/\" y) by WAYBEL_4:13; :: thesis: verum

end;

then (R -below ) . (x "/\" y) = ((R -below ) . x) "/\" ((R -below ) . y) by A2, YELLOW_2:45;
hence R -below preserves_inf_of {x,y} by YELLOW_3:8; :: thesis: verum

end;

end;

assume A6: 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 )
assume A7: ( [a,x] in R & [a,y] in R ) ; :: thesis: [a,(x "/\" y)] in R
R -below preserves_inf_of {x,y} by A6;
then A8: (R -below ) . (x "/\" y) = ((R -below ) . x) "/\" ((R -below ) . y) by YELLOW_3:8
.= ((R -below ) . x) /\ ((R -below ) . y) by YELLOW_2:45 ;
A9: ( (R -below ) . (x "/\" y) = R -below (x "/\" y) & (R -below ) . x = R -below x & (R -below ) . y = R -below y ) by WAYBEL_4:def 13;
( a in R -below x & a in R -below y ) by A7, WAYBEL_4:13;
then a in R -below (x "/\" y) by A8, A9, XBOOLE_0:def 4;
hence [a,(x "/\" y)] in R by WAYBEL_4:13; :: thesis: verum