let X be non empty set ; :: thesis: for A being Subset of X

for S being a_partition of X st A in S holds

union (S \ {A}) = X \ A

let A be Subset of X; :: thesis: for S being a_partition of X st A in S holds

union (S \ {A}) = X \ A

let S be a_partition of X; :: thesis: ( A in S implies union (S \ {A}) = X \ A )

assume A1: A in S ; :: thesis: union (S \ {A}) = X \ A

{A} c= S by A1, TARSKI:def 1;

then reconsider AA = {A} as Subset of S ;

thus union (S \ {A}) = (union S) \ (union AA) by Th43

.= X \ (union {A}) by Def4

.= X \ A ; :: thesis: verum

for S being a_partition of X st A in S holds

union (S \ {A}) = X \ A

let A be Subset of X; :: thesis: for S being a_partition of X st A in S holds

union (S \ {A}) = X \ A

let S be a_partition of X; :: thesis: ( A in S implies union (S \ {A}) = X \ A )

assume A1: A in S ; :: thesis: union (S \ {A}) = X \ A

{A} c= S by A1, TARSKI:def 1;

then reconsider AA = {A} as Subset of S ;

thus union (S \ {A}) = (union S) \ (union AA) by Th43

.= X \ (union {A}) by Def4

.= X \ A ; :: thesis: verum