:: deftheorem Def3 defines carrier-underlaid YELLOW21:def 3 :
for C being category holds
( C is carrier-underlaid iff for a being Object of C ex S being 1-sorted st
( a = S & the_carrier_of a = the carrier of S ) );