[x,y] in [:( the Sorts of (TermAlg S) . s),( the Sorts of (TermAlg S) . s):] by ZFMISC_1:106;
hence '=' is Element of (Equations S) . s by PBOOLE:def 21; :: thesis: verum