let N be non empty with_non-empty_elements set ; :: thesis: for T being InsType of (Trivial-COM N) holds JumpParts T = {0}
let T be InsType of (Trivial-COM N); :: thesis: JumpParts T = {0}
set A = { (JumpPart I) where I is Instruction of (Trivial-COM N) : InsCode I = T } ;
{0} = { (JumpPart I) where I is Instruction of (Trivial-COM N) : InsCode I = T }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (JumpPart I) where I is Instruction of (Trivial-COM N) : InsCode I = T } c= {0}

let a be set ; :: thesis: ( a in {0} implies a in { (JumpPart I) where I is Instruction of (Trivial-COM N) : InsCode I = T } )
assume a in {0} ; :: thesis: a in { (JumpPart I) where I is Instruction of (Trivial-COM N) : InsCode I = T }
then A1: a = 0 by TARSKI:def 1;
A2: the Instructions of (Trivial-COM N) = {[0,0,0]} by Def2;
then A3: InsCodes (Trivial-COM N) = {0} by MCART_1:97;
A4: T = 0 by A3, TARSKI:def 1;
reconsider I = [0,0,0] as Instruction of (Trivial-COM N) by A2, TARSKI:def 1;
A5: JumpPart I = 0 by Th85;
InsCode I = 0 by RECDEF_2:def 1;
hence a in { (JumpPart I) where I is Instruction of (Trivial-COM N) : InsCode I = T } by A1, A4, A5; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (JumpPart I) where I is Instruction of (Trivial-COM N) : InsCode I = T } or a in {0} )
assume a in { (JumpPart I) where I is Instruction of (Trivial-COM N) : InsCode I = T } ; :: thesis: a in {0}
then ex I being Instruction of (Trivial-COM N) st
( a = JumpPart I & InsCode I = T ) ;
then a = 0 by Th85;
hence a in {0} by TARSKI:def 1; :: thesis: verum

end;

hence JumpParts T = {0} ; :: thesis: verum