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, Th20, Th22;
A4: the carrier of AB = the carrier of A /\ the carrier of B by A1, Def3;

now :: thesis: for o being Object of AB
for a being Object of A st o = a holds
idm a in <^o,o^>

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, Th23; :: thesis: verum

end;

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