theorem Th27: :: WAYBEL27:27

for S, T being complete LATTICE
for A being Subset of (UPS (S,T)) holds sup A = "\/" (A,(T |^ the carrier of S))