let L be non empty transitive antisymmetric complete RelStr ; :: thesis: for S being non empty sups-closed Subset of L
for X being Subset of S holds "\/" X,(subrelstr S) = "\/" X,L
let S be non empty sups-closed Subset of L; :: thesis: for X being Subset of S holds "\/" X,(subrelstr S) = "\/" X,L
let X be Subset of S; :: thesis: "\/" X,(subrelstr S) = "\/" X,L
ex_sup_of X,L by YELLOW_0:17;
hence "\/" X,(subrelstr S) = "\/" X,L by Th22; :: thesis: verum