let L be non empty up-complete Poset; :: thesis: for S being non empty full directed-sups-inheriting SubRelStr of L holds S is up-complete
let S be non empty full directed-sups-inheriting SubRelStr of L; :: thesis: S is up-complete

now :: thesis: for X being non empty directed Subset of S holds ex_sup_of X,S

let X be non empty directed Subset of S; :: thesis: ex_sup_of X,S
reconsider Y = X as non empty directed Subset of L by YELLOW_2:7;
ex_sup_of Y,L by WAYBEL_0:75;
hence ex_sup_of X,S by WAYBEL_0:7; :: thesis: verum

end;

hence S is up-complete by WAYBEL_0:75; :: thesis: verum