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 S' = 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 X' = X as Subset of S' ;
A1: X is finite ;
defpred S₁[ set ] means for Y being finite Subset of S' st Y = L holds
( ex_sup_of Y,L & "\/" Y,L = sup Y );
( Bottom L = "\/" {} ,L & Bottom S' = "\/" {} ,S' & ex_sup_of {} ,L ) by YELLOW_0:42;
then A2: S₁[ {} ] by Th64;
A3: 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 & B c= X ) and
A4: for Y being finite Subset of S' st Y = B holds
( ex_sup_of Y,L & "\/" Y,L = sup Y ) ; :: thesis: S₁[B \/ {x}]
let Y be finite Subset of S'; :: thesis: ( Y = B \/ {x} implies ( ex_sup_of Y,L & "\/" Y,L = sup Y ) )
assume A5: Y = B \/ {x} ; :: thesis: ( ex_sup_of Y,L & "\/" Y,L = sup Y )
A6: ( B c= Y & {x} c= Y ) by A5, XBOOLE_1:7;
then reconsider Z = B as finite Subset of S' by XBOOLE_1:1;
A7: ( ex_sup_of Z,L & "\/" Z,L = sup Z ) by A4;
x in Y by A6, ZFMISC_1:37;
then reconsider x = x as Element of S' ;
reconsider a = x as Element of L by YELLOW_0:59;
A8: ex_sup_of {a},L by YELLOW_0:38;
hence ex_sup_of Y,L by A5, A7, YELLOW_2:3; :: thesis: "\/" Y,L = sup Y
( Z = {} or ( Z <> {} & S' is with_suprema ) ) ;
then A9: ( ex_sup_of {x},S' & ex_sup_of Z,S' ) by YELLOW_0:42, YELLOW_0:54;
thus "\/" Y,L = ("\/" Z,L) "\/" (sup {a}) by A5, A7, A8, YELLOW_2:3
.= ("\/" Z,L) "\/" a by YELLOW_0:39
.= (sup Z) "\/" x by A7, YELLOW_0:71
.= (sup Z) "\/" (sup {x}) by YELLOW_0:39
.= sup Y by A5, A9, YELLOW_2:3 ; :: thesis: verum

end;

S₁[X] from FINSET_1:sch 2(A1, A2, A3);
then ( "\/" X,L = sup X' & sup X' in the carrier of S' ) ;
hence ( ex_sup_of X,L implies "\/" X,L in the carrier of S ) ; :: thesis: verum