let S be CatSignature of A; :: thesis: not S is empty
CatSign A is Subsignature of S by Def5;
then the carrier of (CatSign A) c= the carrier of S by INSTALG1:10;
hence not the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: verum