set U = the non empty UAStr ;
set A = the MSAlgebra over S;
set f = the ManySortedMSSet of the Sorts of the MSAlgebra over S, the Sorts of the MSAlgebra over S;
set g = the sort-preserving Function of [:(Union the Sorts of the MSAlgebra over S),(Union [|Y, the Sorts of the MSAlgebra over S|]):],(Union the Sorts of the MSAlgebra over S);
set a = the Function of (Union [|X, the Sorts of T|]), the carrier of the non empty UAStr ;
set eq = the Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of the MSAlgebra over S . the formula-sort of S);
take X = BialgebraStr(# the Sorts of the MSAlgebra over S, the Charact of the MSAlgebra over S, the ManySortedMSSet of the Sorts of the MSAlgebra over S, the Sorts of the MSAlgebra over S, the sort-preserving Function of [:(Union the Sorts of the MSAlgebra over S),(Union [|Y, the Sorts of the MSAlgebra over S|]):],(Union the Sorts of the MSAlgebra over S), the Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of the MSAlgebra over S . the formula-sort of S), the carrier of the non empty UAStr , the charact of the non empty UAStr , the Function of (Union [|X, the Sorts of T|]), the carrier of the non empty UAStr #); :: thesis: not X is 1s-empty
thus not the carrier of X is empty ; :: according to STRUCT_0:def 1 :: thesis: verum