set Q = the non-empty MSAlgebra over J;
set s = the sort-preserving Function of [:(Union the Sorts of the non-empty MSAlgebra over J),(Union [|X, the Sorts of the non-empty MSAlgebra over J|]):],(Union the Sorts of the non-empty MSAlgebra over J);
take K = SubstMSAlgebra(# the Sorts of the non-empty MSAlgebra over J, the Charact of the non-empty MSAlgebra over J, the sort-preserving Function of [:(Union the Sorts of the non-empty MSAlgebra over J),(Union [|X, the Sorts of the non-empty MSAlgebra over J|]):],(Union the Sorts of the non-empty MSAlgebra over J) #); :: thesis: K is non-empty
thus the Sorts of K is V2() ; :: according to MSUALG_1:def 3 :: thesis: verum