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;

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^>

hence
Intersect (A,B) is subcategory of A
by ALTCAT_2:def 14; :: thesis: verumfor 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;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