theorem Th108: :: CLASSES5:106

for U being Universe holds the carrier' of (Ens U) is U -Class