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