len
<*
x
,
y
,
z
*>
=
3
by
FINSEQ_1:45
;
hence
not
<*
x
,
y
,
z
*>
is
trivial
by
NAT_D:60
;
:: thesis:
verum