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

proof

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

end;

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

proof

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

A8: now :: thesis:

let w be set ; :: thesis:
assume A9: w in A ; :: thesis:
then w in S ;
then z misses w by A6, A7, A9, Def4;
hence not y in w by A4, XBOOLE_0:3; :: thesis:

end;

A10: now :: thesis:

assume y in union A ; :: thesis:
then ex v being set st
( y in v & v in A ) by TARSKI:def 4;
hence contradiction by A8; :: thesis:

end;

y in union S by A4, A6, TARSKI:def 4;
hence y in (union S) \ (union A) by A10, XBOOLE_0:def 5; :: thesis:

end;