theorem Th2: :: HILB10_3:2

for n, k being Nat
for i1 being Element of n holds i1 is Element of n + k