let A, B be transitive AltCatStr ; :: thesis: ( A,B have_the_same_composition implies Intersect (A,B) is transitive )

set AB = Intersect (A,B);

assume A1: A,B have_the_same_composition ; :: thesis: Intersect (A,B) is transitive

then A2: the carrier of (Intersect (A,B)) = the carrier of A /\ the carrier of B by Def3;

let o1, o2, o3 be Object of (Intersect (A,B)); :: according to ALTCAT_1:def 2 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )

assume that

A3: <^o1,o2^> <> {} and

A4: <^o2,o3^> <> {} ; :: thesis: not <^o1,o3^> = {}

( dom the Arrows of (Intersect (A,B)) = [: the carrier of (Intersect (A,B)), the carrier of (Intersect (A,B)):] & [o1,o2] in dom the Arrows of (Intersect (A,B)) ) by A3, FUNCT_1:def 2, PARTFUN1:def 2;

then A5: o1 in the carrier of (Intersect (A,B)) by ZFMISC_1:87;

then reconsider A = A, B = B as non empty transitive AltCatStr by A2, XBOOLE_0:def 4;

reconsider b1 = o1, b2 = o2, b3 = o3 as Object of B by A2, A5, XBOOLE_0:def 4;

reconsider a1 = o1, a2 = o2, a3 = o3 as Object of A by A2, A5, XBOOLE_0:def 4;

set f = the Morphism of o1,o2;

set g = the Morphism of o2,o3;

A6: <^o2,o3^> = <^a2,a3^> /\ <^b2,b3^> by A1, Th21;

then A7: ( the Morphism of o2,o3 in <^a2,a3^> & the Morphism of o2,o3 in <^b2,b3^> ) by A4, XBOOLE_0:def 4;

A8: <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> by A1, Th21;

then reconsider f1 = the Morphism of o1,o2 as Morphism of a1,a2 by A3, XBOOLE_0:def 4;

reconsider g2 = the Morphism of o2,o3 as Morphism of b2,b3 by A4, A6, XBOOLE_0:def 4;

reconsider g1 = the Morphism of o2,o3 as Morphism of a2,a3 by A4, A6, XBOOLE_0:def 4;

reconsider f2 = the Morphism of o1,o2 as Morphism of b1,b2 by A3, A8, XBOOLE_0:def 4;

( the Morphism of o1,o2 in <^a1,a2^> & the Morphism of o1,o2 in <^b1,b2^> ) by A3, A8, XBOOLE_0:def 4;

then A9: g1 * f1 = g2 * f2 by A1, A7, Th11;

A10: <^b2,b3^> <> {} by A4, A6;

A11: <^a2,a3^> <> {} by A4, A6;

<^b1,b2^> <> {} by A3, A8;

then A12: <^b1,b3^> <> {} by A10, ALTCAT_1:def 2;

<^a1,a2^> <> {} by A3, A8;

then A13: <^a1,a3^> <> {} by A11, ALTCAT_1:def 2;

<^o1,o3^> = <^a1,a3^> /\ <^b1,b3^> by A1, Th21;

hence not <^o1,o3^> = {} by A13, A12, A9, XBOOLE_0:def 4; :: thesis: verum

set AB = Intersect (A,B);

assume A1: A,B have_the_same_composition ; :: thesis: Intersect (A,B) is transitive

then A2: the carrier of (Intersect (A,B)) = the carrier of A /\ the carrier of B by Def3;

let o1, o2, o3 be Object of (Intersect (A,B)); :: according to ALTCAT_1:def 2 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )

assume that

A3: <^o1,o2^> <> {} and

A4: <^o2,o3^> <> {} ; :: thesis: not <^o1,o3^> = {}

( dom the Arrows of (Intersect (A,B)) = [: the carrier of (Intersect (A,B)), the carrier of (Intersect (A,B)):] & [o1,o2] in dom the Arrows of (Intersect (A,B)) ) by A3, FUNCT_1:def 2, PARTFUN1:def 2;

then A5: o1 in the carrier of (Intersect (A,B)) by ZFMISC_1:87;

then reconsider A = A, B = B as non empty transitive AltCatStr by A2, XBOOLE_0:def 4;

reconsider b1 = o1, b2 = o2, b3 = o3 as Object of B by A2, A5, XBOOLE_0:def 4;

reconsider a1 = o1, a2 = o2, a3 = o3 as Object of A by A2, A5, XBOOLE_0:def 4;

set f = the Morphism of o1,o2;

set g = the Morphism of o2,o3;

A6: <^o2,o3^> = <^a2,a3^> /\ <^b2,b3^> by A1, Th21;

then A7: ( the Morphism of o2,o3 in <^a2,a3^> & the Morphism of o2,o3 in <^b2,b3^> ) by A4, XBOOLE_0:def 4;

A8: <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> by A1, Th21;

then reconsider f1 = the Morphism of o1,o2 as Morphism of a1,a2 by A3, XBOOLE_0:def 4;

reconsider g2 = the Morphism of o2,o3 as Morphism of b2,b3 by A4, A6, XBOOLE_0:def 4;

reconsider g1 = the Morphism of o2,o3 as Morphism of a2,a3 by A4, A6, XBOOLE_0:def 4;

reconsider f2 = the Morphism of o1,o2 as Morphism of b1,b2 by A3, A8, XBOOLE_0:def 4;

( the Morphism of o1,o2 in <^a1,a2^> & the Morphism of o1,o2 in <^b1,b2^> ) by A3, A8, XBOOLE_0:def 4;

then A9: g1 * f1 = g2 * f2 by A1, A7, Th11;

A10: <^b2,b3^> <> {} by A4, A6;

A11: <^a2,a3^> <> {} by A4, A6;

<^b1,b2^> <> {} by A3, A8;

then A12: <^b1,b3^> <> {} by A10, ALTCAT_1:def 2;

<^a1,a2^> <> {} by A3, A8;

then A13: <^a1,a3^> <> {} by A11, ALTCAT_1:def 2;

<^o1,o3^> = <^a1,a3^> /\ <^b1,b3^> by A1, Th21;

hence not <^o1,o3^> = {} by A13, A12, A9, XBOOLE_0:def 4; :: thesis: verum