let A be Subset of T; :: thesis: ( A is subcondensed implies A is 1st_class )
assume A is subcondensed ; :: thesis: A is 1st_class
then Border A is empty by Th26;
hence A is 1st_class by Th47; :: thesis: verum