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