let D be non empty SubCatStr of C; :: thesis: ( D is transitive implies D is associative )
assume D is transitive ; :: thesis: D is associative
then reconsider D = D as non empty transitive SubCatStr of C ;
D is associative
proof
let o1, o2, o3, o4 be Object of D; :: according to ALTCAT_2:def 8 :: thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f)

the carrier of D c= the carrier of C by Def11;
then reconsider p1 = o1, p2 = o2, p3 = o3, p4 = o4 as Object of C ;
let f be Morphism of o1,o2; :: thesis: for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f)

let g be Morphism of o2,o3; :: thesis: for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f)

let h be Morphism of o3,o4; :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} implies (h * g) * f = h * (g * f) )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} and
A3: <^o3,o4^> <> {} ; :: thesis: (h * g) * f = h * (g * f)
A4: <^o2,o3^> c= <^p2,p3^> by Th31;
g in <^o2,o3^> by A2;
then reconsider gg = g as Morphism of p2,p3 by A4;
A5: <^o1,o2^> c= <^p1,p2^> by Th31;
f in <^o1,o2^> by A1;
then reconsider ff = f as Morphism of p1,p2 by A5;
A6: ( <^o1,o3^> <> {} & g * f = gg * ff ) by ;
A7: <^o3,o4^> c= <^p3,p4^> by Th31;
h in <^o3,o4^> by A3;
then reconsider hh = h as Morphism of p3,p4 by A7;
A8: <^p3,p4^> <> {} by ;
A9: ( <^p1,p2^> <> {} & <^p2,p3^> <> {} ) by ;
( <^o2,o4^> <> {} & h * g = hh * gg ) by ;
hence (h * g) * f = (hh * gg) * ff by
.= hh * (gg * ff) by A9, A8, Def8
.= h * (g * f) by A3, A6, Th32 ;
:: thesis: verum
end;
hence D is associative ; :: thesis: verum