theorem Th5: :: MARGREL1:5

for k being Element of NAT holds {} is relation_length of k