let A, B be transitive AltCatStr ; ( 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
; 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)); ALTCAT_1:def 2 ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
assume that
A3:
<^o1,o2^> <> {}
and
A4:
<^o2,o3^> <> {}
; 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; verum