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 )

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 A1: 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 A2: 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 A3: ( 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 A4: ( x = [(x `1 ),(x `2 )] & y = [(y `1 ),(y `2 )] ) by MCART_1:23;
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 A4, FUNCT_5:16
.= [(inf {(x `1 ),(y `1 )}),(inf {(x `2 ),(y `2 )})] by A4, FUNCT_5:16
.= [((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 A1, A2, A3, A4, Th45; :: thesis: verum

end;

end;

assume A5: for S being full SubRelStr of [:L,L:] st the carrier of S = R holds
S is meet-inheriting ; :: thesis: R is multiplicative
reconsider X = R as Subset of [:L,L:] by YELLOW_3:def 2;
A6: X = the carrier of (subrelstr X) by YELLOW_0:def 15;
then A7: subrelstr X is meet-inheriting by A5;
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 )
A8: 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 A6, A7, A8, YELLOW_0:def 16;
then A9: [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 A8, YELLOW_3:47
.= [(inf {a,a}),(inf (proj2 {[a,x],[a,y]}))] by FUNCT_5:16
.= [(inf {a,a}),(inf {x,y})] by FUNCT_5:16
.= [(a "/\" a),(inf {x,y})] by YELLOW_0:40
.= [(a "/\" a),(x "/\" y)] by YELLOW_0:40 ;
hence [a,(x "/\" y)] in R by A9, YELLOW_0:25; :: thesis: verum