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