:: deftheorem Def5 defines mutually-disjoint TAXONOM2:def 5 :
for Y being set holds
( Y is mutually-disjoint iff for x, y being set st x in Y & y in Y & x <> y holds
x misses y );