let C be Category; :: thesis: Alter C is transitive
let o1, o2, o3 be object of (Alter C); :: according to ALTCAT_1:def 4 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: not <^o1,o3^> = {}
reconsider x1 = o1, x2 = o2, x3 = o3 as Object of C ;
A2: <^o1,o2^> = Hom x1,x2 by Def3;
A3: <^o2,o3^> = Hom x2,x3 by Def3;
<^o1,o3^> = Hom x1,x3 by Def3;
hence not <^o1,o3^> = {} by A1, A2, A3, CAT_1:52; :: thesis: verum