let p be preProgram of S; :: thesis: ( p is empty implies p is halt-free )
assume p is empty ; :: thesis: p is halt-free
hence not halt S in rng p ; :: according to COMPOS_1:def 3 :: thesis: verum