let p be PartState of S; :: thesis: ( p is halting & not p is program-free implies not p is halt-free )
F: rng (ProgramPart p) c= rng p by RELAT_1:99;
assume ( p is halting & not p is program-free ) ; :: thesis: not p is halt-free
then not ProgramPart p is halt-free ;
then halt S in rng (ProgramPart p) by COMPOS_1:def 7;
hence halt S in rng p by F; :: according to COMPOS_1:def 7 :: thesis: verum