theorem Th25: :: WAYBEL24:25

for S being non empty RelStr
for T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S)
for i being Element of S holds (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)