let L be non empty transitive RelStr ; :: thesis: for S being non empty full directed-sups-inheriting SubRelStr of L
for R being non empty directed-sups-inheriting SubRelStr of S holds R is directed-sups-inheriting SubRelStr of L
let S be non empty full directed-sups-inheriting SubRelStr of L; :: thesis: for R being non empty directed-sups-inheriting SubRelStr of S holds R is directed-sups-inheriting SubRelStr of L
let R be non empty directed-sups-inheriting SubRelStr of S; :: thesis: R is directed-sups-inheriting SubRelStr of L
reconsider T = R as SubRelStr of L by YELLOW_6:16;
T is directed-sups-inheriting

proof

let X be directed Subset of T; :: according to WAYBEL_0:def 4 :: thesis: ( X = {} or not ex_sup_of X,L or "\/" X,L in the carrier of T )
reconsider Y = X as directed Subset of S by YELLOW_2:7;
assume A1: X <> {} ; :: thesis: ( not ex_sup_of X,L or "\/" X,L in the carrier of T )
assume ex_sup_of X,L ; :: thesis: "\/" X,L in the carrier of T
then ( sup Y = "\/" X,L & ex_sup_of Y,S ) by A1, WAYBEL_0:7;
hence "\/" X,L in the carrier of T by A1, WAYBEL_0:def 4; :: thesis: verum

end;

hence R is directed-sups-inheriting SubRelStr of L ; :: thesis: verum