let S be SubRelStr of L; :: thesis: ( S is finite-sups-inheriting implies ( S is bottom-inheriting & S is join-inheriting ) )
assume A1: S is finite-sups-inheriting ; :: thesis: ( S is bottom-inheriting & S is join-inheriting )
then ( ( ex_sup_of {} ,L implies "\/" ({} S),L in the carrier of S ) & ex_sup_of {} ,L ) by Def18, YELLOW_0:42;
hence Bottom L in the carrier of S ; :: according to WAYBEL34:def 19 :: thesis: S is join-inheriting
let x, y be Element of L; :: 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},L or "\/" {x,y},L 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},L or "\/" {x,y},L in the carrier of S )
then reconsider X = {x,y} as finite Subset of S by ZFMISC_1:38;
( ex_sup_of X,L implies "\/" X,L in the carrier of S ) by A1, Def18;
hence ( not ex_sup_of {x,y},L or "\/" {x,y},L in the carrier of S ) ; :: thesis: verum