:: deftheorem Def9 defines POSAltCat ORDERS_3:def 9 :
for P being non empty POSet_set
for b₂ being strict AltCatStr holds
( b₂ = POSAltCat P iff ( the carrier of b₂ = P & ( for i, j being Element of P holds
( the Arrows of b₂ . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of b₂ . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) ) );