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, Th64; :: thesis: verum