assume the carrier of (CatSign A) = {} ; :: according to INSTALG1:def 1 :: thesis: the carrier' of (CatSign A) = {}
then A1: [:{0 },(2 -tuples_on A):] = {} by Def5;
A = {} by A1;
then ( 1 <> 0 & 3 <> 0 implies ( 1 -tuples_on A = {} & 3 -tuples_on A = {} ) ) by Th7;
then ( [:{1},(1 -tuples_on A):] = {} & [:{2},(3 -tuples_on A):] = {} ) by ZFMISC_1:113;
then [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] = {} ;
hence the carrier' of (CatSign A) = {} by Def5; :: thesis: verum