let L be non empty Poset; :: thesis: for S being non empty full directed-sups-inheriting SubRelStr of L
for X being non empty set holds S |^ X is directed-sups-inheriting SubRelStr of L |^ X
let S be non empty full directed-sups-inheriting SubRelStr of L; :: thesis: for X being non empty set holds S |^ X is directed-sups-inheriting SubRelStr of L |^ X
let X be non empty set ; :: thesis: S |^ X is directed-sups-inheriting SubRelStr of L |^ X
reconsider SX = S |^ X as non empty full SubRelStr of L |^ X by Th38;
defpred S₁[ set , non empty reflexive RelStr ] means $1 is non empty directed Subset of $2;

A1: now :: thesis: for A being Subset of (S |^ X) st S₁[A,S |^ X] holds
for i being Element of X holds S₁[ pi (A,i),S]

let A be Subset of (S |^ X); :: thesis: ( S₁[A,S |^ X] implies for i being Element of X holds S₁[ pi (A,i),S] )
assume S₁[A,S |^ X] ; :: thesis: for i being Element of X holds S₁[ pi (A,i),S]
then reconsider B = A as non empty directed Subset of (S |^ X) ;
let i be Element of X; :: thesis: S₁[ pi (A,i),S]
(X --> S) . i = S ;
then pi (B,i) is non empty directed Subset of S by Th34;
hence S₁[ pi (A,i),S] ; :: thesis: verum

end;

A2: now :: thesis: for X being Subset of S st S₁[X,S] holds
S inherits_sup_of X,L

let X be Subset of S; :: thesis: ( S₁[X,S] implies S inherits_sup_of X,L )
assume S₁[X,S] ; :: thesis: S inherits_sup_of X,L
then ( ex_sup_of X,L implies ( ex_sup_of X,S & sup X = "\/" (X,L) ) ) by WAYBEL_0:7;
hence S inherits_sup_of X,L ; :: thesis: verum

end;

SX is directed-sups-inheriting

proof

let A be directed Subset of SX; :: according to WAYBEL_0:def 4 :: thesis: ( A = {} or not ex_sup_of A,L |^ X or "\/" (A,(L |^ X)) in the carrier of SX )
for A being Subset of (S |^ X) st S₁[A,S |^ X] holds
S |^ X inherits_sup_of A,L |^ X from YELLOW16:sch 2(A1, A2);
then ( A <> {} implies S |^ X inherits_sup_of A,L |^ X ) ;
hence ( A = {} or not ex_sup_of A,L |^ X or "\/" (A,(L |^ X)) in the carrier of SX ) ; :: thesis: verum

end;

hence S |^ X is directed-sups-inheriting SubRelStr of L |^ X ; :: thesis: verum