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