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 object ; :: according to TARSKI:def 3 :: thesis: ( not y in (union S) \ (union A) or y in union (S \ A) )
assume A1: y in (union S) \ (union A) ; :: thesis: y in union (S \ A)
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: verum

end;

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

proof

let y be object ; :: 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
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: for w being set st w in A holds
not y in w

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

end;

A10: now :: thesis: not y in union A

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

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: verum

end;