theorem Th6: :: WAYBEL24:6

for S being RelStr
for T being non empty RelStr
for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T