theorem Th8: :: TSEP_2:8

for X being non empty 1-sorted
for A, A1, A2 being Subset of X st A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition holds
A1 = A2