let T be Semilattice; for S being non empty full SubRelStr of T holds
( S is meet-inheriting iff for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S )
let S be non empty full SubRelStr of T; ( S is meet-inheriting iff for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S )
hereby ( ( for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S ) implies S is meet-inheriting )
assume A1:
S is
meet-inheriting
;
for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of Slet X be non
empty finite Subset of
S;
"/\" (X,T) in the carrier of SA2:
X is
finite
;
defpred S1[
set ]
means ( $1
<> {} implies
"/\" ($1,
T)
in the
carrier of
S );
A3:
S1[
{} ]
;
A4:
now let y,
x be
set ;
( y in X & x c= X & S1[x] implies S1[x \/ {y}] )assume that A5:
y in X
and A6:
x c= X
and A7:
S1[
x]
;
S1[x \/ {y}]thus
S1[
x \/ {y}]
verumproof
assume
x \/ {y} <> {}
;
"/\" ((x \/ {y}),T) in the carrier of S
reconsider y9 =
y as
Element of
S by A5;
reconsider z =
y9 as
Element of
T by YELLOW_0:59;
A8:
x c= the
carrier of
S
by A6, XBOOLE_1:1;
the
carrier of
S c= the
carrier of
T
by YELLOW_0:def 13;
then reconsider x9 =
x as
finite Subset of
T by A6, A8, XBOOLE_1:1;
A9:
ex_inf_of {z},
T
by YELLOW_0:38;
A10:
inf {z} = y9
by YELLOW_0:39;
now assume A11:
x9 <> {}
;
inf (x9 \/ {z}) in the carrier of Sthen
ex_inf_of x9,
T
by YELLOW_0:55;
then A12:
inf (x9 \/ {z}) = (inf x9) "/\" z
by A9, A10, YELLOW_2:4;
ex_inf_of {(inf x9),z},
T
by YELLOW_0:21;
then
inf {(inf x9),z} in the
carrier of
S
by A1, A7, A11, YELLOW_0:def 16;
hence
inf (x9 \/ {z}) in the
carrier of
S
by A12, YELLOW_0:40;
verum end;
hence
"/\" (
(x \/ {y}),
T)
in the
carrier of
S
by A10;
verum
end; end;
S1[
X]
from FINSET_1:sch 2(A2, A3, A4);
hence
"/\" (
X,
T)
in the
carrier of
S
;
verum
end;
assume A13:
for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S
; S is meet-inheriting
let x, y be Element of T; 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},T or "/\" ({x,y},T) in the carrier of S )
assume that
A14:
x in the carrier of S
and
A15:
y in the carrier of S
; ( not ex_inf_of {x,y},T or "/\" ({x,y},T) in the carrier of S )
{x,y} c= the carrier of S
by A14, A15, ZFMISC_1:38;
hence
( not ex_inf_of {x,y},T or "/\" ({x,y},T) in the carrier of S )
by A13; verum