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:7;
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 A2: ex_sup_of X,L ; :: thesis: "\/" (X,L) in the carrier of T
then A3: ex_sup_of Y,S by A1, WAYBEL_0:7;
sup Y = "\/" (X,L) by A1, A2, WAYBEL_0:7;
hence "\/" (X,L) in the carrier of T by A1, A3, WAYBEL_0:def 4; :: thesis: verum

end;

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