let S be full SubRelStr of L; :: thesis: ( S is bottom-inheriting & S is join-inheriting implies S is finite-sups-inheriting )
assume ( S is bottom-inheriting & S is join-inheriting ) ; :: thesis: 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; :: according to WAYBEL34:def 18 :: thesis: ( 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 S₁[ 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: S₁[ {} ] by A2, Th60, YELLOW_0:42;
A4: for x, B being set st x in X & B c= X & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in X & B c= X & S₁[B] implies S₁[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 ) ; :: thesis: S₁[B \/ {x}]
let Y be finite Subset of S9; :: thesis: ( Y = B \/ {x} implies ( ex_sup_of Y,L & "\/" (Y,L) = sup Y ) )
assume A6: Y = B \/ {x} ; :: thesis: ( 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; :: thesis: "\/" (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 ; :: thesis: verum

end;

S₁[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 ) ; :: thesis: verum