:: deftheorem Def14 defines EnsCat ALTCAT_1:def 14 :
for A being non empty set
for b₂ being non empty strict pseudo-functional AltCatStr holds
( b₂ = EnsCat A iff ( the carrier of b₂ = A & ( for a1, a2 being Object of b₂ holds <^a1,a2^> = Funcs (a1,a2) ) ) );