for X being non empty 1-sorted
for A1, A2 being Subset of X st ( A1 = A2 ` or A2 = A1 ` ) holds
A1,A2 constitute_a_decomposition