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

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