consider C being image of A such that
A1: C is bool-correct 4,1 integer MSAlgebra over S by Def1;
take C ; :: thesis: C is bool-correct
thus C is bool-correct by A1; :: thesis: verum