let A be Subset of T; :: thesis: ( A is subcondensed implies A is semi-open )
assume A is subcondensed ; :: thesis: A is semi-open
then A c= Cl (Int A) by Th9;
hence A is semi-open by DECOMP_1:def 2; :: thesis: verum