let A, B be category; :: thesis:
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:
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;

let o be Object of AB; :: thesis:
let a be Object of A; :: thesis:
reconsider b = o as Object of B by A4, XBOOLE_0:def 4;
assume A5: o = a ; :: thesis:
then idm a = idm b by A3;
hence idm a in <^o,o^> by A1, A5, Th23; :: thesis:

end;