set C = the non-empty bool-correct 4,1 integer MSAlgebra over S;
reconsider C1 = the non-empty bool-correct 4,1 integer MSAlgebra over S as image of the non-empty bool-correct 4,1 integer MSAlgebra over S by Th6;
take the non-empty bool-correct 4,1 integer MSAlgebra over S ; :: thesis: the non-empty bool-correct 4,1 integer MSAlgebra over S is integer
take C1 ; :: according to AOFA_A01:def 1 :: thesis: C1 is bool-correct 4,1 integer MSAlgebra over S
thus C1 is bool-correct 4,1 integer MSAlgebra over S ; :: thesis: verum