let P be a_partition of X; :: thesis: P is mutually-disjoint
let x, y be set ; :: according to TAXONOM2:def 5 :: thesis: ( not x in P or not y in P or x = y or x misses y )
thus ( not x in P or not y in P or x = y or x misses y ) by EQREL_1:def 4; :: thesis: verum