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 {{}} ; :: according to CATALG_1:def 4 :: thesis: ( CatSign {{}} is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on {{}}):] )
thus ( CatSign {{}} is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on {{}}):] ) by Def3, INSTALG1:15; :: thesis: verum

end;

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