let l1, l2 be Instruction-Location of SCMPDS ; :: thesis: ( l1 <> l2 implies locnum l1 <> locnum l2 )
assume A1: ( l1 <> l2 & locnum l1 = locnum l2 ) ; :: thesis: contradiction
( il. (locnum l1) = l1 & il. (locnum l2) = l2 ) by Def1;
hence contradiction by A1; :: thesis: verum