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 Th41;
defpred S₁[ set , non empty reflexive RelStr ] means $1 is non empty directed Subset of $2;

A1: now

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 by FUNCOP_1:13;
then pi B,i is non empty directed Subset of S by Th37;
hence S₁[ pi A,i,S] ; :: thesis: verum

end;

A2: now

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 by Th42; :: 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 ) by Def6; :: thesis: verum

end;

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