let L be lower-bounded LATTICE; :: thesis: for R being auxiliary Relation of L holds
( R is multiplicative iff for x being Element of L holds R -above x is filtered )
let R be auxiliary Relation of L; :: thesis: ( R is multiplicative iff for x being Element of L holds R -above x is filtered )

hereby :: thesis: ( ( for x being Element of L holds R -above x is filtered ) implies R is multiplicative )

assume A1: R is multiplicative ; :: thesis: for x being Element of L holds R -above x is filtered
let x be Element of L; :: thesis: R -above x is filtered
thus R -above x is filtered :: thesis: verum

proof

let y, z be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( not y in R -above x or not z in R -above x or ex b₁ being Element of the carrier of L st
( b₁ in R -above x & b₁ <= y & b₁ <= z ) )
assume ( y in R -above x & z in R -above x ) ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in R -above x & b₁ <= y & b₁ <= z )
then ( [x,y] in R & [x,z] in R ) by WAYBEL_4:14;
then [x,(y "/\" z)] in R by A1, Def7;
then ( y "/\" z in R -above x & y >= y "/\" z & z >= y "/\" z ) by WAYBEL_4:14, YELLOW_0:23;
hence ex b₁ being Element of the carrier of L st
( b₁ in R -above x & b₁ <= y & b₁ <= z ) ; :: thesis: verum

end;

end;

assume A2: for x being Element of L holds R -above x is filtered ; :: 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 ( [a,x] in R & [a,y] in R ) ; :: thesis: [a,(x "/\" y)] in R
then ( x in R -above a & y in R -above a & R -above a is filtered ) by A2, WAYBEL_4:14;
then x "/\" y in R -above a by WAYBEL_0:41;
hence [a,(x "/\" y)] in R by WAYBEL_4:14; :: thesis: verum