SubFrom a,b = [3,{} ,<*a,b*>] by SCMFSA10:11;
hence JumpPart (SubFrom a,b) is empty by RECDEF_2:def 2; :: according to AMISTD_2:def 13 :: thesis: verum