take
{
[
0
,
{}
,
{}
]
,
[
1,
{}
,
{}
]
}
;
:: thesis:
not
{
[
0
,
{}
,
{}
]
,
[
1,
{}
,
{}
]
}
is
trivial
[
0
,
{}
,
{}
]
<>
[
1,
{}
,
{}
]
by
XTUPLE_0:3
;
hence
not
{
[
0
,
{}
,
{}
]
,
[
1,
{}
,
{}
]
}
is
trivial
by
CHAIN_1:3
;
:: thesis:
verum