let X be set ; :: thesis: for D being a_partition of X
for P being Subset of D holds union (D \ P) = (union D) \ (union P)
let D be a_partition of X; :: thesis: for P being Subset of D holds union (D \ P) = (union D) \ (union P)
let P be Subset of D; :: thesis: union (D \ P) = (union D) \ (union P)
thus union (D \ P) c= (union D) \ (union P) :: according to XBOOLE_0:def 10 :: thesis: (union D) \ (union P) c= union (D \ P)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (D \ P) or x in (union D) \ (union P) )
assume x in union (D \ P) ; :: thesis: x in (union D) \ (union P)
then consider y being set such that
A2: x in y and
A3: y in D \ P by TARSKI:def 4;
( y in D & not y in P ) by A3, XBOOLE_0:def 5;
then A4: x in union D by A2, TARSKI:def 4;
not x in union P
proof
assume x in union P ; :: thesis: contradiction
then consider z being set such that
A5: x in z and
A6: z in P by TARSKI:def 4;
( z in D & y in D ) by A3, A6, XBOOLE_0:def 5;
then ( y = z or y misses z ) by EQREL_1:def 4;
hence contradiction by A2, A5, A6, A3, XBOOLE_0:def 4, XBOOLE_0:def 5; :: thesis: verum
end;
hence x in (union D) \ (union P) by A4, XBOOLE_0:def 5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union D) \ (union P) or x in union (D \ P) )
assume x in (union D) \ (union P) ; :: thesis: x in union (D \ P)
then A7: ( x in union D & not x in union P ) by XBOOLE_0:def 5;
then consider y being set such that
A8: x in y and
A9: y in D by TARSKI:def 4;
y in D \ P
proof
assume not y in D \ P ; :: thesis: contradiction
then ( y in P or not y in D ) by XBOOLE_0:def 5;
hence contradiction by A7, A8, A9, TARSKI:def 4; :: thesis: verum
end;
hence x in union (D \ P) by A8, TARSKI:def 4; :: thesis: verum