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 & the Arrows of (Intersect A,B) = Intersect the Arrows of A,the Arrows of B & the Comp of (Intersect A,B) = Intersect the Comp of A,the Comp of B ) by Def3;
let o1, o2, o3 be object of (Intersect A,B); :: according to ALTCAT_1:def 4 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
assume A3: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: not <^o1,o3^> = {}
A4: dom the Arrows of (Intersect A,B) = [:the carrier of (Intersect A,B),the carrier of (Intersect A,B):] by PARTFUN1:def 4;
( [o1,o2] in dom the Arrows of (Intersect A,B) & [o2,o3] in dom the Arrows of (Intersect A,B) ) by A3, FUNCT_1:def 4;
then A5: ( o1 in the carrier of (Intersect A,B) & o2 in the carrier of (Intersect A,B) & o3 in the carrier of (Intersect A,B) ) by A4, ZFMISC_1:106;
then ( o1 in the carrier of A & o2 in the carrier of A & o3 in the carrier of A & o1 in the carrier of B & o2 in the carrier of B & o3 in the carrier of B ) by A2, XBOOLE_0:def 4;
then reconsider A = A, B = B as non empty transitive AltCatStr ;
reconsider a1 = o1, a2 = o2, a3 = o3 as object of A by A2, A5, XBOOLE_0:def 4;
reconsider b1 = o1, b2 = o2, b3 = o3 as object of B by A2, A5, XBOOLE_0:def 4;
A6: ( <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> & <^o2,o3^> = <^a2,a3^> /\ <^b2,b3^> & <^o1,o3^> = <^a1,a3^> /\ <^b1,b3^> ) by A1, Th22;
then ( <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^b1,b2^> <> {} & <^b2,b3^> <> {} ) by A3;
then A7: ( <^a1,a3^> <> {} & <^b1,b3^> <> {} ) by ALTCAT_1:def 4;
consider f being Morphism of o1,o2, g being Morphism of o2,o3;
A8: ( f in <^a1,a2^> & f in <^b1,b2^> & g in <^a2,a3^> & g in <^b2,b3^> ) by A3, A6, XBOOLE_0:def 4;
reconsider f1 = f as Morphism of a1,a2 by A3, A6, XBOOLE_0:def 4;
reconsider f2 = f as Morphism of b1,b2 by A3, A6, XBOOLE_0:def 4;
reconsider g1 = g as Morphism of a2,a3 by A3, A6, XBOOLE_0:def 4;
reconsider g2 = g as Morphism of b2,b3 by A3, A6, XBOOLE_0:def 4;
g1 * f1 = g2 * f2 by A1, A8, Th11;
hence not <^o1,o3^> = {} by A6, A7, XBOOLE_0:def 4; :: thesis: verum