:: deftheorem Def2 defines /\ CAT_5:def 2 :
for C1, C2 being Category st ex C being Category st
( C1 is Subcategory of C & C2 is Subcategory of C ) & ex o1 being Object of C1 st o1 is Object of C2 holds
for b₃ being strict Category holds
( b₃ = C1 /\ C2 iff ( the carrier of b₃ = the carrier of C1 /\ the carrier of C2 & the carrier' of b₃ = the carrier' of C1 /\ the carrier' of C2 & the Source of b₃ = the Source of C1 | the carrier' of C2 & the Target of b₃ = the Target of C1 | the carrier' of C2 & the Comp of b₃ = the Comp of C1 || the carrier' of C2 ) );