let L be non empty complete Poset; :: thesis: for S being non empty full SubRelStr of L
for X being Subset of S st "\/" X,L in the carrier of S holds
"\/" X,S = "\/" X,L
let S be non empty full SubRelStr of L; :: thesis: for X being Subset of S st "\/" X,L in the carrier of S holds
"\/" X,S = "\/" X,L
let X be Subset of S; :: thesis: ( "\/" X,L in the carrier of S implies "\/" X,S = "\/" X,L )
assume A1: "\/" X,L in the carrier of S ; :: thesis: "\/" X,S = "\/" X,L
ex_sup_of X,L by Th17;
hence "\/" X,S = "\/" X,L by A1, Th65; :: thesis: verum