let C be category; :: thesis: for B being non empty subcategory of C

for A being non empty subcategory of B holds A is non empty subcategory of C

let B be non empty subcategory of C; :: thesis: for A being non empty subcategory of B holds A is non empty subcategory of C

let A be non empty subcategory of B; :: thesis: A is non empty subcategory of C

reconsider D = A as non empty with_units SubCatStr of C by ALTCAT_2:21;

for A being non empty subcategory of B holds A is non empty subcategory of C

let B be non empty subcategory of C; :: thesis: for A being non empty subcategory of B holds A is non empty subcategory of C

let A be non empty subcategory of B; :: thesis: A is non empty subcategory of C

reconsider D = A as non empty with_units SubCatStr of C by ALTCAT_2:21;

now :: thesis: for o being Object of D

for o1 being Object of C st o = o1 holds

idm o1 in <^o,o^>

hence
A is non empty subcategory of C
by ALTCAT_2:def 14; :: thesis: verumfor o1 being Object of C st o = o1 holds

idm o1 in <^o,o^>

let o be Object of D; :: thesis: for o1 being Object of C st o = o1 holds

idm o1 in <^o,o^>

let o1 be Object of C; :: thesis: ( o = o1 implies idm o1 in <^o,o^> )

assume A1: o = o1 ; :: thesis: idm o1 in <^o,o^>

( o in the carrier of D & the carrier of D c= the carrier of B ) by ALTCAT_2:def 11;

then reconsider oo = o as Object of B ;

idm o = idm oo by ALTCAT_2:34

.= idm o1 by A1, ALTCAT_2:34 ;

hence idm o1 in <^o,o^> ; :: thesis: verum

end;idm o1 in <^o,o^>

let o1 be Object of C; :: thesis: ( o = o1 implies idm o1 in <^o,o^> )

assume A1: o = o1 ; :: thesis: idm o1 in <^o,o^>

( o in the carrier of D & the carrier of D c= the carrier of B ) by ALTCAT_2:def 11;

then reconsider oo = o as Object of B ;

idm o = idm oo by ALTCAT_2:34

.= idm o1 by A1, ALTCAT_2:34 ;

hence idm o1 in <^o,o^> ; :: thesis: verum