:: deftheorem Def9 defines with_halt COMPOS_0:def 10 :
for X being set holds
( X is with_halt iff [0,{},{}] in X );