let it1, it2 be Element of NAT ; :: thesis: ( CurInstr p,(Comput p,s,it1) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
it1 <= k ) & CurInstr p,(Comput p,s,it2) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
it2 <= k ) implies it1 = it2 )
assume A4: ( CurInstr p,(Comput p,s,it1) = halt S & ( for k being Element of NAT st CurInstr p,(Comput p,s,k) = halt S holds
it1 <= k ) & CurInstr p,(Comput p,s,it2) = halt S & ( for k being Element of 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 A4, XXREAL_0:1; :: thesis: verum