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 b1 being Element of the carrier of L st
( b1 in R -above x & b1 <= y & b1 <= z ) )
assume ( y in R -above x & z in R -above x ) ; :: thesis: ex b1 being Element of the carrier of L st
( b1 in R -above x & b1 <= y & b1 <= z )
then ( [x,y] in R & [x,z] in R ) by WAYBEL_4:14;
then [x,(y "/\" z)] in R by A1;
then A2: y "/\" z in R -above x by WAYBEL_4:14;
( y >= y "/\" z & z >= y "/\" z ) by YELLOW_0:23;
hence ex b1 being Element of the carrier of L st
( b1 in R -above x & b1 <= y & b1 <= z ) by A2; :: thesis: verum
end;
end;
assume A3: 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 A4: ( x in R -above a & y in R -above a ) by WAYBEL_4:14;
R -above a is filtered by A3;
then x "/\" y in R -above a by A4, WAYBEL_0:41;
hence [a,(x "/\" y)] in R by WAYBEL_4:14; :: thesis: verum