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