n in NAT by ORDINAL1:def 12;
then conv A is bounded by Th14;
hence conv A is compact ; :: thesis: verum