[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