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

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