let L be non empty up-complete Poset; :: thesis: for S1, S2 being non empty full directed-sups-inheriting SubRelStr of L st S1 is SubRelStr of S2 holds
S1 is full directed-sups-inheriting SubRelStr of S2
let S1, S2 be non empty full directed-sups-inheriting SubRelStr of L; :: thesis: ( S1 is SubRelStr of S2 implies S1 is full directed-sups-inheriting SubRelStr of S2 )
assume S1 is SubRelStr of S2 ; :: thesis: S1 is full directed-sups-inheriting SubRelStr of S2
then reconsider S = S1 as SubRelStr of S2 ;
S is directed-sups-inheriting

proof

let X be directed Subset of S; :: according to WAYBEL_0:def 4 :: thesis: ( X = {} or not ex_sup_of X,S2 or "\/" (X,S2) in the carrier of S )
assume X <> {} ; :: thesis: ( not ex_sup_of X,S2 or "\/" (X,S2) in the carrier of S )
then reconsider Y1 = X as non empty directed Subset of S1 ;
reconsider Y2 = Y1 as non empty directed Subset of S2 by YELLOW_2:7;
reconsider Y = Y1 as non empty directed Subset of L by YELLOW_2:7;
A1: ex_sup_of Y,L by WAYBEL_0:75;
then A2: sup Y = sup Y1 by WAYBEL_0:7;
sup Y2 = sup Y by A1, WAYBEL_0:7;
hence ( not ex_sup_of X,S2 or "\/" (X,S2) in the carrier of S ) by A2; :: thesis: verum

end;

hence S1 is full directed-sups-inheriting SubRelStr of S2 by Th25; :: thesis: verum