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 that
A2: [a,x] in R and
A3: [b,y] in R ; :: thesis: [(a "/\" b),(x "/\" y)] in R
( a "/\" b <= b & y <= y ) by YELLOW_0:23;
then A4: [(a "/\" b),y] in R by A3, WAYBEL_4:def 4;
( a >= a "/\" b & x <= x ) by YELLOW_0:23;
then [(a "/\" b),x] in R by A2, WAYBEL_4:def 4;
hence [(a "/\" b),(x "/\" y)] in R by A1, A4; :: thesis: verum
end;
assume A5: 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 A5; :: thesis: verum