theorem :: TAXONOM2:9

{{}} is mutually-disjoint by Lm2;