the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def 8;
hence ComplRelStr R is finite ; :: thesis: verum