let L be lower-bounded LATTICE; 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; ( 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 ( ( 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
;
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:];
( the carrier of S = R implies S is meet-inheriting )assume A3:
the
carrier of
S = R
;
S is meet-inheriting thus
S is
meet-inheriting
verumproof
let x,
y be
Element of
[:L,L:];
YELLOW_0:def 16 ( 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 )
;
( 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;
verum
end;
end;
assume
for S being full SubRelStr of [:L,L:] st the carrier of S = R holds
S is meet-inheriting
; R is multiplicative
then A6:
subrelstr X is meet-inheriting
by A1;
let a, x, y be Element of L; WAYBEL_7:def 7 ( [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 )
; [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; verum