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)

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

thus
union (S \ A) c= (union S) \ (union A)
:: thesis: verum
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;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

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;

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

end;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

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;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

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

y in union S
by A4, A6, TARSKI:def 4;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;then ex v being set st

( y in v & v in A ) by TARSKI:def 4;

hence contradiction by A8; :: thesis: verum

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