theorem :: EQREL_1:44

for X being non empty set
for A being Subset of X
for S being a_partition of X st A in S holds
union (S \ {A}) = X \ A