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