theorem Th16: :: PRALG_1:17

for S being 1-sorted holds Carrier <*S*> = <* the carrier of S*>