ProperPrefixes p, dom p are_equipotent by Th67;
hence ProperPrefixes p is finite by CARD_1:68; :: thesis: verum