take S = CatSign {{} }; :: thesis: ( S is Categorial & not S is empty & S is strict )
thus S is Categorial :: thesis: ( not S is empty & S is strict )

proof

take A = {{} }; :: according to CATALG_1:def 6 :: thesis: ( CatSign A is Subsignature of S & the carrier of S = [:{0 },(2 -tuples_on A):] )
thus ( CatSign A is Subsignature of S & the carrier of S = [:{0 },(2 -tuples_on A):] ) by Def5, INSTALG1:16; :: thesis: verum

end;

thus ( not S is empty & S is strict ) ; :: thesis: verum