let X be non empty set ; :: thesis: for S being a_partition of X
for A being Subset of S holds (union S) \ (union A) = union (S \ A)
let S be a_partition of X; :: thesis: for A being Subset of S holds (union S) \ (union A) = union (S \ A)
let A be Subset of S; :: thesis: (union S) \ (union A) = union (S \ A)
thus (union S) \ (union A) c= union (S \ A) :: according to XBOOLE_0:def 10 :: thesis: union (S \ A) c= (union S) \ (union A)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (union S) \ (union A) or y in union (S \ A) )
assume y in (union S) \ (union A) ; :: thesis: y in union (S \ A)
then A1: ( y in union S & not y in union A ) by XBOOLE_0:def 5;
then consider z being set such that
A2: ( y in z & z in S ) by TARSKI:def 4;
not z in A by A1, A2, TARSKI:def 4;
then ( y in z & z in S \ A ) by A2, XBOOLE_0:def 5;
hence y in union (S \ A) by TARSKI:def 4; :: thesis: verum

end;

thus union (S \ A) c= (union S) \ (union A) :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in union (S \ A) or y in (union S) \ (union A) )
assume y in union (S \ A) ; :: thesis: y in (union S) \ (union A)
then consider z being set such that
A3: ( y in z & z in S \ A ) by TARSKI:def 4;
A4: ( y in z & z in S & not z in A ) by A3, XBOOLE_0:def 5;
then A5: y in union S by TARSKI:def 4;

A6: now

let w be set ; :: thesis: ( w in A implies not y in w )
assume A7: w in A ; :: thesis: not y in w
then w in S ;
then z misses w by A4, A7, Def6;
hence not y in w by A3, XBOOLE_0:3; :: thesis: verum

end;

now

assume y in union A ; :: thesis: contradiction
then consider v being set such that
A8: ( y in v & v in A ) by TARSKI:def 4;
thus contradiction by A6, A8; :: thesis: verum

end;

hence y in (union S) \ (union A) by A5, XBOOLE_0:def 5; :: thesis: verum

end;