let it1, it2 be Nat; :: thesis: ( CurInstr (p,(Comput (p,s,it1))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds
it1 <= k ) & CurInstr (p,(Comput (p,s,it2))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds
it2 <= k ) implies it1 = it2 )
assume A5: ( CurInstr (p,(Comput (p,s,it1))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds
it1 <= k ) & CurInstr (p,(Comput (p,s,it2))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds
it2 <= k ) & not it1 = it2 ) ; :: thesis: contradiction
then ( it1 <= it2 & it2 <= it1 ) ;
hence contradiction by A5, XXREAL_0:1; :: thesis: verum