consider s being Element of (CatSign A);
let S be CatSignature of A; :: thesis: not S is empty
CatSign A is Subsignature of S by Def7;
then the carrier of (CatSign A) c= the carrier of S by INSTALG1:11;
hence not the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: verum