let L be non empty transitive RelStr ; 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; 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; 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;
WAYBEL_0:def 4 ( 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 <> {}
;
( not ex_sup_of X,L or "\/" (X,L) in the carrier of T )
assume A2:
ex_sup_of X,
L
;
"\/" (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;
verum
end;
hence
R is directed-sups-inheriting SubRelStr of L
; verum