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