theorem Th64: :: YELLOW_0:64

for L being non empty transitive RelStr
for S being non empty full SubRelStr of L
for X being Subset of S st ex_sup_of X,L & "\/" (X,L) in the carrier of S holds
( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) )