let S be SubRelStr of L; :: thesis: ( S is sups-inheriting implies S is finite-sups-inheriting )
assume A1: S is sups-inheriting ; :: thesis: S is finite-sups-inheriting
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 )
thus ( ex_sup_of X,L implies "\/" (X,L) in the carrier of S ) by A1, YELLOW_0:def 19; :: thesis: verum