let x be Element of {[0,{},{}],[1,{},{}]}; :: thesis: JumpPart x = {}
( x = [0,{},{}] or x = [1,{},{}] ) by TARSKI:def 2;
hence JumpPart x = {} ; :: thesis: verum