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