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