let
A
be
QC-alphabet
;
:: thesis:
index
(
VERUM
A
)
=
0
A
VERUM
A
is
closed
by
QC_LANG3:20
;
hence
index
(
VERUM
A
)
=
0
A
by
Th20
;
:: thesis:
verum