let T be TopSpace; :: thesis: for A being Subset of T st A is open holds
A is subcondensed
let A be Subset of T; :: thesis: ( A is open implies A is subcondensed )
assume A is open ; :: thesis: A is subcondensed
then Cl (Int A) = Cl A by TOPS_1:23;
hence A is subcondensed by Def2; :: thesis: verum