thus
ObCat o is transitive
not ObCat o is empty proof
let o1,
o2,
o3 be
Object of
(ObCat o);
ALTCAT_1:def 2 ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
assume that
<^o1,o2^> <> {}
and A1:
<^o2,o3^> <> {}
;
not <^o1,o3^> = {}
o1 = o
by Th23;
hence
not
<^o1,o3^> = {}
by A1, Th23;
verum
end;
the carrier of (ObCat o) = {o}
by Def12;
hence
not the carrier of (ObCat o) is empty
; STRUCT_0:def 1 verum