let L be non empty complete Poset; 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; 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; ( "\/" (X,L) in the carrier of S implies "\/" (X,S) = "\/" (X,L) )
assume A1:
"\/" (X,L) in the carrier of S
; "\/" (X,S) = "\/" (X,L)
ex_sup_of X,L
by Th17;
hence
"\/" (X,S) = "\/" (X,L)
by A1, Th64; verum