theorem :: SCMPDS_2:82

for i being Element of NAT holds IC <> dl. i