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 Function-like & the Element of the Sorts of (FreeMSA X) . v is Relation-like )
thus ( the Element of the Sorts of (FreeMSA X) . v is Function-like & the Element of the Sorts of (FreeMSA X) . v is Relation-like ) ; :: thesis: verum