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