let T be TopSpace; :: thesis: for A being Subset of T holds
( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) )
let A be Subset of T; :: thesis: ( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) )
thus ( A is condensed implies ( Int (Cl A) c= A & A c= Cl (Int A) ) ) by Th8, Th9; :: thesis: ( Int (Cl A) c= A & A c= Cl (Int A) implies A is condensed )
assume ( Int (Cl A) c= A & A c= Cl (Int A) ) ; :: thesis: A is condensed
then ( A is supercondensed & A is subcondensed ) by Th8, Th9;
hence A is condensed ; :: thesis: verum