set a = the Element of the Sorts of A . s;
take the Element of the Sorts of A . s ; :: thesis: the Element of the Sorts of A . s is s -sort
thus the Element of the Sorts of A . s in the Sorts of A . s ; :: according to MSAFREE5:def 10 :: thesis: verum