set S = Trivial-COM ;
halt Trivial-COM = [0,{},{}] by Def1;
hence JumpPart (halt Trivial-COM) is empty by RECDEF_2:def 2; :: according to COMPOS_1:def 16,COMPOS_1:def 18 :: thesis: verum