let R be NatRelStr of n; :: thesis: R is finite
the carrier of R = n by LNRS;
hence R is finite ; :: thesis: verum