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