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 S1[ 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 S1[A,S |^ X] holds
for i being Element of X holds S1[ pi (A,i),S]
let A be Subset of (S |^ X); :: thesis: ( S1[A,S |^ X] implies for i being Element of X holds S1[ pi (A,i),S] )
assume S1[A,S |^ X] ; :: thesis: for i being Element of X holds S1[ pi (A,i),S]
then reconsider B = A as non empty directed Subset of (S |^ X) ;
let i be Element of X; :: thesis: S1[ pi (A,i),S]
(X --> S) . i = S ;
then pi (B,i) is non empty directed Subset of S by Th34;
hence S1[ pi (A,i),S] ; :: thesis: verum
end;
A2: now :: thesis: for X being Subset of S st S1[X,S] holds
S inherits_sup_of X,L
let X be Subset of S; :: thesis: ( S1[X,S] implies S inherits_sup_of X,L )
assume S1[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 S1[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