let T be InsType of {[0,{},{}]}; JumpParts T = {0}
set A = { (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T } ;
{0} = { (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T }
proof
hereby TARSKI:def 3,
XBOOLE_0:def 10 { (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T } c= {0}
let a be
object ;
( a in {0} implies a in { (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T } )assume
a in {0}
;
a in { (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T } then A1:
a = 0
by TARSKI:def 1;
A2:
InsCodes {[0,{},{}]} = {0}
by MCART_1:92;
A3:
T = 0
by A2, TARSKI:def 1;
reconsider I =
[0,0,0] as
Element of
{[0,{},{}]} by TARSKI:def 1;
A4:
JumpPart I = 0
;
InsCode I = 0
;
hence
a in { (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T }
by A1, A3, A4;
verum
end;
let a be
object ;
TARSKI:def 3 ( not a in { (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T } or a in {0} )
assume
a in { (JumpPart I) where I is Element of {[0,{},{}]} : InsCode I = T }
;
a in {0}
then consider I being
Element of
{[0,{},{}]} such that A5:
(
a = JumpPart I &
InsCode I = T )
;
I = [0,{},{}]
by TARSKI:def 1;
then
a = 0
by A5;
hence
a in {0}
by TARSKI:def 1;
verum
end;
hence
JumpParts T = {0}
; verum