let A, B be category; :: thesis: ( A,B have_the_same_composition & not Intersect A,B is empty & ( for a being object of
for b being object of st a = b holds
idm a = idm b ) implies Intersect A,B is subcategory of )
assume that
A1: A,B have_the_same_composition and
A2: not Intersect A,B is empty and
A3: for a being object of
for b being object of st a = b holds
idm a = idm b ; :: thesis: Intersect A,B is subcategory of
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 ; :: thesis: for a being object of st o = a holds
idm a in <^o,o^>
let a be object of ; :: thesis: ( o = a implies idm a in <^o,o^> )
reconsider b = o as object of 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 by ALTCAT_2:def 14; :: thesis: verum