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 ;
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 ;
reconsider b1 = o1, b2 = o2, b3 = o3 as Object of B by ;
reconsider a1 = o1, a2 = o2, a3 = o3 as Object of A by ;
set f = the Morphism of o1,o2;
set g = the Morphism of o2,o3;
A6: <^o2,o3^> = <^a2,a3^> /\ <^b2,b3^> by ;
then A7: ( the Morphism of o2,o3 in <^a2,a3^> & the Morphism of o2,o3 in <^b2,b3^> ) by ;
A8: <^o1,o2^> = <^a1,a2^> /\ <^b1,b2^> by ;
then reconsider f1 = the Morphism of o1,o2 as Morphism of a1,a2 by ;
reconsider g2 = the Morphism of o2,o3 as Morphism of b2,b3 by ;
reconsider g1 = the Morphism of o2,o3 as Morphism of a2,a3 by ;
reconsider f2 = the Morphism of o1,o2 as Morphism of b1,b2 by ;
( the Morphism of o1,o2 in <^a1,a2^> & the Morphism of o1,o2 in <^b1,b2^> ) by ;
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 ;
<^a1,a2^> <> {} by A3, A8;
then A13: <^a1,a3^> <> {} by ;
<^o1,o3^> = <^a1,a3^> /\ <^b1,b3^> by ;
hence not <^o1,o3^> = {} by ; :: thesis: verum