set e = the Element of the Sorts of (FreeMSA X) . v;
take the Element of the Sorts of (FreeMSA X) . v ; :: thesis: the Element of the Sorts of (FreeMSA X) . v is finite
thus the Element of the Sorts of (FreeMSA X) . v is finite ; :: thesis: verum