let B be non empty subcategory of A; :: thesis: B is carrier-underlaid
let b be Object of B; :: according to YELLOW21:def 3 :: thesis: ex S being 1-sorted st
( b = S & the_carrier_of b = the carrier of S )
reconsider a = b as Object of A by ALTCAT_2:29;
consider S being 1-sorted such that
A1: a = S and
A2: the_carrier_of a = the carrier of S by Def3;
take S ; :: thesis: ( b = S & the_carrier_of b = the carrier of S )
thus b = S by A1; :: thesis: the_carrier_of b = the carrier of S
thus the_carrier_of b = the carrier of S by A2, ALTCAT_2:34; :: thesis: verum