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

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