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 4 ( <^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 4, PARTFUN1:def 4;
then A5:
o1 in the carrier of (Intersect A,B)
by ZFMISC_1:106;
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;
consider f being Morphism of o1,o2, g being Morphism of o2,o3;
A6:
<^o2,o3^> = <^a2,a3^> /\ <^b2,b3^>
by A1, Th22;
then A7:
( g in <^a2,a3^> & g in <^b2,b3^> )
by A4, XBOOLE_0:def 4;
A8:
<^o1,o2^> = <^a1,a2^> /\ <^b1,b2^>
by A1, Th22;
then reconsider f1 = f as Morphism of a1,a2 by A3, XBOOLE_0:def 4;
reconsider g2 = g as Morphism of b2,b3 by A4, A6, XBOOLE_0:def 4;
reconsider g1 = g as Morphism of a2,a3 by A4, A6, XBOOLE_0:def 4;
reconsider f2 = f as Morphism of b1,b2 by A3, A8, XBOOLE_0:def 4;
( f in <^a1,a2^> & f 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 4;
<^a1,a2^> <> {}
by A3, A8;
then A13:
<^a1,a3^> <> {}
by A11, ALTCAT_1:def 4;
<^o1,o3^> = <^a1,a3^> /\ <^b1,b3^>
by A1, Th22;
hence
not <^o1,o3^> = {}
by A13, A12, A9, XBOOLE_0:def 4; verum