theorem Th1: :: MSALIMIT:1

for P being non empty Poset
for i, j, k being Element of P
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF st i >= j & j >= k holds
(bind (B,j,k)) ** (bind (B,i,j)) = bind (B,i,k)