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;

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 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

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;

end;

assume for S being full SubRelStr of [:L,L:] st the carrier of S = R holds
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