let C be category; :: thesis: for B being non empty subcategory of non empty
for A being non empty subcategory of non empty holds A is non empty subcategory of non empty
let B be non empty subcategory of non empty ; :: thesis: for A being non empty subcategory of non empty holds A is non empty subcategory of non empty
let A be non empty subcategory of non empty ; :: thesis: A is non empty subcategory of non empty
reconsider D = A as non empty with_units SubCatStr of C by ALTCAT_2:22;

now

let o be object of ; :: thesis: for o1 being object of st o = o1 holds
idm o1 in <^o,o^>
let o1 be object of ; :: 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 ;
idm o = idm oo by ALTCAT_2:35
.= idm o1 by A1, ALTCAT_2:35 ;
hence idm o1 in <^o,o^> ; :: thesis: verum

end;

hence A is non empty subcategory of non empty by ALTCAT_2:def 14; :: thesis: verum