take halt S ; :: thesis: halt S is halting
thus halt S is halting ; :: thesis: verum