:: deftheorem defines POSCat ORDERS_3:def 8 :
for P being non empty POSet_set
for b₂ being strict with_triple-like_morphisms Category holds
( b₂ = POSCat P iff ( the carrier of b₂ = P & ( for a, b being Element of P
for f being Element of Funcs (Carr P) st f in MonFuncs (a,b) holds
[[a,b],f] is Morphism of b₂ ) & ( for m being Morphism of b₂ ex a, b being Element of P ex f being Element of Funcs (Carr P) st
( m = [[a,b],f] & f in MonFuncs (a,b) ) ) & ( for m1, m2 being Morphism of b₂
for a1, a2, a3 being Element of P
for f1, f2 being Element of Funcs (Carr P) st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],(f2 * f1)] ) ) );