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;
now :: thesis: for o being Object of D
for 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;
hence A is non empty subcategory of C by ALTCAT_2:def 14; :: thesis: verum