let D be SubCatStr of C; ( D is full & not D is empty implies D is transitive )
assume A1:
( D is full & not D is empty )
; D is transitive
let o1, o2, o3 be Object of D; ALTCAT_1:def 2 ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
assume A2:
( <^o1,o2^> <> {} & <^o2,o3^> <> {} )
; not <^o1,o3^> = {}
reconsider p1 = o1, p2 = o2, p3 = o3 as Object of C by A1, Th29;
( <^p1,p2^> <> {} & <^p2,p3^> <> {} )
by A1, A2, Th28;
then
<^p1,p3^> <> {}
by ALTCAT_1:def 2;
hence
not <^o1,o3^> = {}
by A1, Th28; verum