let A, B be category; :: thesis: ( A,B have_the_same_composition & not Intersect A,B is empty & ( for a being object of A
for b being object of B st a = b holds
idm a = idm b ) implies Intersect A,B is subcategory of A )
assume that
A1: A,B have_the_same_composition and
A2: not Intersect A,B is empty and
A3: for a being object of A
for b being object of B st a = b holds
idm a = idm b ; :: thesis: Intersect A,B is subcategory of A
reconsider AB = Intersect A,B as non empty transitive SubCatStr of A by A1, A2, Th21, Th23;
A4: the carrier of AB = the carrier of A /\ the carrier of B by A1, Def3;

now

let o be object of AB; :: thesis: for a being object of A st o = a holds
idm a in <^o,o^>
let a be object of A; :: thesis: ( o = a implies idm a in <^o,o^> )
reconsider b = o as object of B by A4, XBOOLE_0:def 4;
assume A5: o = a ; :: thesis: idm a in <^o,o^>
then idm a = idm b by A3;
hence idm a in <^o,o^> by A1, A5, Th24; :: thesis: verum

end;

hence Intersect A,B is subcategory of A by ALTCAT_2:def 14; :: thesis: verum