take CatSign {{} } ; :: thesis: ( CatSign {{} } is delta-concrete & not CatSign {{} } is empty & CatSign {{} } is strict )
thus ( CatSign {{} } is delta-concrete & not CatSign {{} } is empty & CatSign {{} } is strict ) ; :: thesis: verum