let S be SubRelStr of L; :: thesis: ( S is sups-inheriting implies S is directed-sups-inheriting )
assume A2: for X being Subset of S st ex_sup_of X,L holds
"\/" (X,L) in the carrier of S ; :: according to YELLOW_0:def 19 :: thesis: S is directed-sups-inheriting
let X be directed Subset of S; :: according to WAYBEL_0:def 4 :: thesis: ( X <> {} & ex_sup_of X,L implies "\/" (X,L) in the carrier of S )
thus ( X <> {} & ex_sup_of X,L implies "\/" (X,L) in the carrier of S ) by A2; :: thesis: verum