reconsider S = C as Subsignature of C by INSTALG1:15;
take S ; :: thesis: S is constructor
thus S is constructor ; :: thesis: verum