for X being set
for P being a_partition of X
for x, a, b being set st x in a & a in P & x in b & b in P holds
a = b by Def4, XBOOLE_0:3;