theorem :: AMI_3:13

for i being Nat holds
( IC <> dl. i & IC <> i ) by Th1;