FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 16;
hence the Sorts of (FreeMSA X) is disjoint_valued ; :: thesis: verum