let P be a_partition of X; :: thesis: P is mutually-disjoint
for x, y being set st x in P & y in P & x <> y holds
x misses y by EQREL_1:def 4;
hence P is mutually-disjoint by TAXONOM2:def 5; :: thesis: verum