let S be full SubRelStr of L; ( S is bottom-inheriting & S is join-inheriting implies S is finite-sups-inheriting )
assume
( S is bottom-inheriting & S is join-inheriting )
; S is finite-sups-inheriting
then reconsider S9 = S as full join-inheriting bottom-inheriting SubRelStr of L ;
let X be finite Subset of S; WAYBEL34:def 18 ( ex_sup_of X,L implies "\/" (X,L) in the carrier of S )
reconsider X9 = X as Subset of S9 ;
A1:
X is finite
;
defpred S1[ set ] means for Y being finite Subset of S9 st Y = L holds
( ex_sup_of Y,L & "\/" (Y,L) = sup Y );
A2:
Bottom L = "\/" ({},L)
;
Bottom S9 = "\/" ({},S9)
;
then A3:
S1[ {} ]
by A2, Th60, YELLOW_0:42;
A4:
for x, B being set st x in X & B c= X & S1[B] holds
S1[B \/ {x}]
proof
let x,
B be
set ;
( x in X & B c= X & S1[B] implies S1[B \/ {x}] )
assume that
x in X
and
B c= X
and A5:
for
Y being
finite Subset of
S9 st
Y = B holds
(
ex_sup_of Y,
L &
"\/" (
Y,
L)
= sup Y )
;
S1[B \/ {x}]
let Y be
finite Subset of
S9;
( Y = B \/ {x} implies ( ex_sup_of Y,L & "\/" (Y,L) = sup Y ) )
assume A6:
Y = B \/ {x}
;
( ex_sup_of Y,L & "\/" (Y,L) = sup Y )
A7:
B c= Y
by A6, XBOOLE_1:7;
A8:
{x} c= Y
by A6, XBOOLE_1:7;
reconsider Z =
B as
finite Subset of
S9 by A7, XBOOLE_1:1;
A9:
ex_sup_of Z,
L
by A5;
A10:
"\/" (
Z,
L)
= sup Z
by A5;
x in Y
by A8, ZFMISC_1:31;
then reconsider x =
x as
Element of
S9 ;
reconsider a =
x as
Element of
L by YELLOW_0:58;
A11:
ex_sup_of {a},
L
by YELLOW_0:38;
hence
ex_sup_of Y,
L
by A6, A9, YELLOW_2:3;
"\/" (Y,L) = sup Y
A12:
(
Z = {} or (
Z <> {} &
S9 is
with_suprema ) )
;
A13:
ex_sup_of {x},
S9
by YELLOW_0:54;
A14:
ex_sup_of Z,
S9
by A12, YELLOW_0:42, YELLOW_0:54;
thus "\/" (
Y,
L) =
("\/" (Z,L)) "\/" (sup {a})
by A6, A9, A11, YELLOW_2:3
.=
("\/" (Z,L)) "\/" a
by YELLOW_0:39
.=
(sup Z) "\/" x
by A10, YELLOW_0:70
.=
(sup Z) "\/" (sup {x})
by YELLOW_0:39
.=
sup Y
by A6, A13, A14, YELLOW_2:3
;
verum
end;
S1[X]
from FINSET_1:sch 2(A1, A3, A4);
then
"\/" (X,L) = sup X9
;
hence
( ex_sup_of X,L implies "\/" (X,L) in the carrier of S )
; verum