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

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