let T be TopSpace; :: thesis: for A being Subset of T holds
( A is condensed iff ( A is subcondensed & A is supercondensed ) )
let A be Subset of T; :: thesis: ( A is condensed iff ( A is subcondensed & A is supercondensed ) )
thus ( A is condensed implies ( A is subcondensed & A is supercondensed ) ) :: thesis: ( A is subcondensed & A is supercondensed implies A is condensed )

proof

assume A is condensed ; :: thesis: ( A is subcondensed & A is supercondensed )
then ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) by Def3;
hence ( A is subcondensed & A is supercondensed ) by Def1, Def2; :: thesis: verum

end;

assume ( A is subcondensed & A is supercondensed ) ; :: thesis: A is condensed
then ( Int (Cl A) = Int A & Cl (Int A) = Cl A ) by Def1, Def2;
hence A is condensed by Def3; :: thesis: verum