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

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