let X be set ; :: thesis: ( X is mutually-disjoint implies X \ {{}} is a_partition of union X )
assume A1: X is mutually-disjoint ; :: thesis: X \ {{}} is a_partition of union X
now :: thesis: for x being object st x in X \ {{}} holds
x in bool (union X)
let x be object ; :: thesis: ( x in X \ {{}} implies x in bool (union X) )
reconsider y = x as set by TARSKI:1;
assume x in X \ {{}} ; :: thesis: x in bool (union X)
then y c= union X by ZFMISC_1:74;
hence x in bool (union X) ; :: thesis: verum
end;
then A2: X \ {{}} is Subset of (bool (union X)) by TARSKI:def 3;
now :: thesis: ( union (X \ {{}}) = union X & ( for A being Subset of (union X) st A in X \ {{}} holds
( A <> {} & ( for B being Subset of (union X) st B in X \ {{}} & A <> B holds
A misses B ) ) ) )
thus union (X \ {{}}) = union X by PARTIT1:2; :: thesis: for A being Subset of (union X) st A in X \ {{}} holds
( A <> {} & ( for B being Subset of (union X) st B in X \ {{}} & A <> B holds
A misses B ) )
let A be Subset of (union X); :: thesis: ( A in X \ {{}} implies ( A <> {} & ( for B being Subset of (union X) st B in X \ {{}} & A <> B holds
A misses B ) ) )
assume A3: A in X \ {{}} ; :: thesis: ( A <> {} & ( for B being Subset of (union X) st B in X \ {{}} & A <> B holds
A misses B ) )
then not A in {{}} by XBOOLE_0:def 5;
hence A <> {} by TARSKI:def 1; :: thesis: for B being Subset of (union X) st B in X \ {{}} & A <> B holds
A misses B
let B be Subset of (union X); :: thesis: ( B in X \ {{}} & A <> B implies A misses B )
assume ( B in X \ {{}} & A <> B ) ; :: thesis: A misses B
hence A misses B by A1, A3, TAXONOM2:def 5; :: thesis: verum
end;
hence X \ {{}} is a_partition of union X by A2, EQREL_1:def 4; :: thesis: verum