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