let D be SubCatStr of C; :: thesis: ( D is full & not D is empty implies D is transitive )

assume A1: ( D is full & not D is empty ) ; :: thesis: D is transitive

let o1, o2, o3 be Object of D; :: according to ALTCAT_1:def 2 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )

assume A2: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: 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; :: thesis: verum

assume A1: ( D is full & not D is empty ) ; :: thesis: D is transitive

let o1, o2, o3 be Object of D; :: according to ALTCAT_1:def 2 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )

assume A2: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: 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; :: thesis: verum