consider loc being Instruction-Location of S;
reconsider h = halt S as Element of ObjectKind loc by Def14;
loc in NAT by Def4;
then reconsider l = loc as Element of ObjectKind (IC S) by Def11;
( (IC S),loc --> l,h is autonomic & (IC S),loc --> l,h is halting ) by Th65, Th67;
hence ex b₁ being FinPartState of S st
( b₁ is autonomic & b₁ is halting ) ; :: thesis: verum