theorem Th32: :: YELLOW18:32

for A being non empty set
for a being Object of (EnsCat A) holds the_carrier_of a = a