let S be SubRelStr of A; :: thesis: S is finite
the carrier of S c= the carrier of A by YELLOW_0:def 13;
hence S is finite ; :: thesis: verum