:: deftheorem Def1 defines OrderedAlgFam MSALIMIT:def 1 :
for P being non empty Poset
for S being non empty non void ManySortedSign
for b₃ being MSAlgebra-Family of the carrier of P,S holds
( b₃ is OrderedAlgFam of P,S iff ex F being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (b₃ . i),(b₃ . j) ex f2 being ManySortedFunction of (b₃ . j),(b₃ . k) st
( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism b₃ . i,b₃ . j ) );