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 that
<^o1,o2^> <> {} and
A1: <^o2,o3^> <> {} ; :: thesis: not <^o1,o3^> = {}
o1 = o by Th24;
hence not <^o1,o3^> = {} by A1, Th24; :: 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