theorem Th8: :: TOPS_5:8

for I being 2 -element set
for i, j being Element of I st i <> j holds
I = {i,j}