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