let L be lower-bounded LATTICE; :: thesis: for R being auxiliary Relation of L holds

( R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds

S is meet-inheriting )

let R be auxiliary Relation of L; :: thesis: ( R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds

S is meet-inheriting )

reconsider X = R as Subset of [:L,L:] by YELLOW_3:def 2;

A1: X = the carrier of (subrelstr X) by YELLOW_0:def 15;

S is meet-inheriting ; :: thesis: R is multiplicative

then A6: subrelstr X is meet-inheriting by A1;

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 )

A7: ex_inf_of {[a,x],[a,y]},[:L,L:] by YELLOW_0:21;

assume ( [a,x] in R & [a,y] in R ) ; :: thesis: [a,(x "/\" y)] in R

then inf {[a,x],[a,y]} in R by A1, A6, A7;

then A8: [a,x] "/\" [a,y] in R by YELLOW_0:40;

set ax = [a,x];

set ay = [a,y];

[a,x] "/\" [a,y] = inf {[a,x],[a,y]} by YELLOW_0:40

.= [(inf (proj1 {[a,x],[a,y]})),(inf (proj2 {[a,x],[a,y]}))] by A7, YELLOW_3:47

.= [(inf {a,a}),(inf (proj2 {[a,x],[a,y]}))] by FUNCT_5:13

.= [(inf {a,a}),(inf {x,y})] by FUNCT_5:13

.= [(a "/\" a),(inf {x,y})] by YELLOW_0:40

.= [(a "/\" a),(x "/\" y)] by YELLOW_0:40 ;

hence [a,(x "/\" y)] in R by A8, YELLOW_0:25; :: thesis: verum

( R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds

S is meet-inheriting )

let R be auxiliary Relation of L; :: thesis: ( R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds

S is meet-inheriting )

reconsider X = R as Subset of [:L,L:] by YELLOW_3:def 2;

A1: X = the carrier of (subrelstr X) by YELLOW_0:def 15;

hereby :: thesis: ( ( for S being full SubRelStr of [:L,L:] st the carrier of S = R holds

S is meet-inheriting ) implies R is multiplicative )

assume
for S being full SubRelStr of [:L,L:] st the carrier of S = R holds S is meet-inheriting ) implies R is multiplicative )

assume A2:
R is multiplicative
; :: thesis: for S being full SubRelStr of [:L,L:] st the carrier of S = R holds

S is meet-inheriting

let S be full SubRelStr of [:L,L:]; :: thesis: ( the carrier of S = R implies S is meet-inheriting )

assume A3: the carrier of S = R ; :: thesis: S is meet-inheriting

thus S is meet-inheriting :: thesis: verum

end;S is meet-inheriting

let S be full SubRelStr of [:L,L:]; :: thesis: ( the carrier of S = R implies S is meet-inheriting )

assume A3: the carrier of S = R ; :: thesis: S is meet-inheriting

thus S is meet-inheriting :: thesis: verum

proof

let x, y be Element of [:L,L:]; :: according to YELLOW_0:def 16 :: thesis: ( not x in the carrier of S or not y in the carrier of S or not ex_inf_of {x,y},[:L,L:] or "/\" ({x,y},[:L,L:]) in the carrier of S )

assume A4: ( x in the carrier of S & y in the carrier of S ) ; :: thesis: ( not ex_inf_of {x,y},[:L,L:] or "/\" ({x,y},[:L,L:]) in the carrier of S )

the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by YELLOW_3:def 2;

then A5: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by MCART_1:21;

ex_inf_of {x,y},[:L,L:] by YELLOW_0:21;

then inf {x,y} = [(inf (proj1 {x,y})),(inf (proj2 {x,y}))] by YELLOW_3:47

.= [(inf {(x `1),(y `1)}),(inf (proj2 {x,y}))] by A5, FUNCT_5:13

.= [(inf {(x `1),(y `1)}),(inf {(x `2),(y `2)})] by A5, FUNCT_5:13

.= [((x `1) "/\" (y `1)),(inf {(x `2),(y `2)})] by YELLOW_0:40

.= [((x `1) "/\" (y `1)),((x `2) "/\" (y `2))] by YELLOW_0:40 ;

hence ( not ex_inf_of {x,y},[:L,L:] or "/\" ({x,y},[:L,L:]) in the carrier of S ) by A2, A3, A4, A5, Th41; :: thesis: verum

end;assume A4: ( x in the carrier of S & y in the carrier of S ) ; :: thesis: ( not ex_inf_of {x,y},[:L,L:] or "/\" ({x,y},[:L,L:]) in the carrier of S )

the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by YELLOW_3:def 2;

then A5: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by MCART_1:21;

ex_inf_of {x,y},[:L,L:] by YELLOW_0:21;

then inf {x,y} = [(inf (proj1 {x,y})),(inf (proj2 {x,y}))] by YELLOW_3:47

.= [(inf {(x `1),(y `1)}),(inf (proj2 {x,y}))] by A5, FUNCT_5:13

.= [(inf {(x `1),(y `1)}),(inf {(x `2),(y `2)})] by A5, FUNCT_5:13

.= [((x `1) "/\" (y `1)),(inf {(x `2),(y `2)})] by YELLOW_0:40

.= [((x `1) "/\" (y `1)),((x `2) "/\" (y `2))] by YELLOW_0:40 ;

hence ( not ex_inf_of {x,y},[:L,L:] or "/\" ({x,y},[:L,L:]) in the carrier of S ) by A2, A3, A4, A5, Th41; :: thesis: verum

S is meet-inheriting ; :: thesis: R is multiplicative

then A6: subrelstr X is meet-inheriting by A1;

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 )

A7: ex_inf_of {[a,x],[a,y]},[:L,L:] by YELLOW_0:21;

assume ( [a,x] in R & [a,y] in R ) ; :: thesis: [a,(x "/\" y)] in R

then inf {[a,x],[a,y]} in R by A1, A6, A7;

then A8: [a,x] "/\" [a,y] in R by YELLOW_0:40;

set ax = [a,x];

set ay = [a,y];

[a,x] "/\" [a,y] = inf {[a,x],[a,y]} by YELLOW_0:40

.= [(inf (proj1 {[a,x],[a,y]})),(inf (proj2 {[a,x],[a,y]}))] by A7, YELLOW_3:47

.= [(inf {a,a}),(inf (proj2 {[a,x],[a,y]}))] by FUNCT_5:13

.= [(inf {a,a}),(inf {x,y})] by FUNCT_5:13

.= [(a "/\" a),(inf {x,y})] by YELLOW_0:40

.= [(a "/\" a),(x "/\" y)] by YELLOW_0:40 ;

hence [a,(x "/\" y)] in R by A8, YELLOW_0:25; :: thesis: verum