:: deftheorem Def11 defines with_binary_products CAT_8:def 11 :
for C being category holds
( C is with_binary_products iff for a, b being Object of C ex d being Object of C ex p1 being Morphism of d,a ex p2 being Morphism of d,b st
( Hom (d,a) <> {} & Hom (d,b) <> {} & d,p1,p2 is_product_of a,b ) );