let s be State of SCM+FSA ; :: according to AMI_1:def 26 :: thesis: ( not Initialized I c= s or ProgramPart s halts_on s )
assume Initialized I c= s ; :: thesis: ProgramPart s halts_on s
hence ProgramPart s halts_on s by Th19; :: thesis: verum