let i be Element of NAT ; :: thesis: ( IC SCMPDS <> dl. i & IC SCMPDS <> i )

hereby :: thesis: IC SCMPDS <> i

assume IC SCMPDS = dl. i ; :: thesis: contradiction
then NAT = [1,i] by Th6, AMI_3:def 19;
hence contradiction by ARYTM_3:36; :: thesis: verum

end;

assume IC SCMPDS = i ; :: thesis: contradiction
then NAT = i by Th6;
then NAT in NAT ;
hence contradiction ; :: thesis: verum