reconsider T = S as Subsignature of S by Th16;
take T ; :: thesis: not T is void
thus not T is void ; :: thesis: verum