let T be sup-Semilattice; :: thesis: for S being non empty full SubRelStr of T holds
( S is join-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 join-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 join-inheriting )
assume A1:
S is
join-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}]then reconsider y' =
y as
Element of
S ;
reconsider z =
y' as
Element of
T by YELLOW_0:59;
thus
S1[
x \/ {y}]
:: thesis: verumproof
assume
x \/ {y} <> {}
;
:: thesis: "\/" (x \/ {y}),T in the carrier of S
(
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_sup_of {z},
T &
sup {z} = y' )
by YELLOW_0:38, YELLOW_0:39;
now assume A7:
x' <> {}
;
:: thesis: sup (x' \/ {z}) in the carrier of Sthen
ex_sup_of x',
T
by YELLOW_0:54;
then A8:
(
sup x' in the
carrier of
S &
sup (x' \/ {z}) = (sup x') "\/" z &
ex_sup_of {(sup x'),z},
T )
by A5, A6, A7, YELLOW_0:20, YELLOW_2:3;
then
sup {(sup x'),z} in the
carrier of
S
by A1, YELLOW_0:def 17;
hence
sup (x' \/ {z}) in the
carrier of
S
by A8, YELLOW_0:41;
:: 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 join-inheriting
let x, y be Element of T; :: according to YELLOW_0:def 17 :: thesis: ( not x in the carrier of S or not y in the carrier of S or not ex_sup_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_sup_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_sup_of {x,y},T or "\/" {x,y},T in the carrier of S )
by A9; :: thesis: verum