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 by Def1;
hence contradiction by A1, Def1; :: thesis: verum