ex C being image of A st C is bool-correct 4,1 integer MSAlgebra over S by Def1;
hence ex b₁ being bool-correct image of A st b₁ is 4,1 integer ; :: thesis: verum