thus ObCat o is transitive :: thesis: not ObCat o is empty

proof

let o1, o2, o3 be object of (ObCat o); :: 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^> = {}
( o1 = o & o2 = o ) by Th24;
hence not <^o1,o3^> = {} by A1; :: thesis: verum

end;

the carrier of (ObCat o) = {o} by Def12;
hence not the carrier of (ObCat o) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum