theorem :: EQREL_1:69

for X being non empty set
for D being non empty a_partition of X
for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds
B c= W ) holds
W = (proj D) " ((proj D) .: W)