:: deftheorem Def20 defines DiscrCat ALTCAT_1:def 20 :
for A being non empty set
for b₂ being non empty strict quasi-discrete AltCatStr holds
( b₂ = DiscrCat A iff ( the carrier of b₂ = A & ( for i being Object of b₂ holds <^i,i^> = {(id i)} ) ) );