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