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 Th23;
hence A is 1st_class by Th37; :: thesis: verum