let A be Subset of T; :: thesis: ( A is supercondensed implies A is 1st_class )
assume A is supercondensed ; :: thesis: A is 1st_class
then Border A is empty by Th22;
hence A is 1st_class by Th37; :: thesis: verum