set U1 = the non-empty MSAlgebra over S;
set X = the Sorts of the non-empty MSAlgebra over S;
take FreeMSA the Sorts of the non-empty MSAlgebra over S ; :: thesis: ( FreeMSA the Sorts of the non-empty MSAlgebra over S is free & FreeMSA the Sorts of the non-empty MSAlgebra over S is strict )
thus ( FreeMSA the Sorts of the non-empty MSAlgebra over S is free & FreeMSA the Sorts of the non-empty MSAlgebra over S is strict ) by Th17; :: thesis: verum