theorem Th20: :: FINSEQ_3:20

for k being Nat
for y being object st Seg k = {y} holds
( k = 1 & y = 1 )