theorem :: FINSEQ_3:21

for x, y being object
for k being Nat st Seg k = {x,y} & x <> y holds
( k = 2 & {x,y} = {1,2} )