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

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

proof

the carrier of (ObCat o) = {o}
by Def12;
let o1, o2, o3 be Object of (ObCat o); :: according to ALTCAT_1:def 2 :: 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 Th23;

hence not <^o1,o3^> = {} by A1, Th23; :: thesis: verum

end;assume that

<^o1,o2^> <> {} and

A1: <^o2,o3^> <> {} ; :: thesis: not <^o1,o3^> = {}

o1 = o by Th23;

hence not <^o1,o3^> = {} by A1, Th23; :: thesis: verum

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