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