theorem Th3: :: TSEP_2:3

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