theorem :: ORDERS_3:8

for f being 1-sorted holds Carr {f} = { the carrier of f}