the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def3;
hence not the carrier of (CatSign A) is empty ; :: according to STRUCT_0:def 1 :: thesis: not CatSign A is void
the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3;
hence not the carrier' of (CatSign A) is empty ; :: according to STRUCT_0:def 13 :: thesis: verum