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