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 A1: A is condensed ; :: thesis: ( A is subcondensed & A is supercondensed )
then A2: Int (Cl A) = Int A by Def3;
Cl (Int A) = Cl A by A1, Def3;
hence ( A is subcondensed & A is supercondensed ) by A2, Def1, Def2; :: thesis: verum

end;

assume that
A3: A is subcondensed and
A4: A is supercondensed ; :: thesis: A is condensed
A5: Cl (Int A) = Cl A by A3, Def2;
Int (Cl A) = Int A by A4, Def1;
hence A is condensed by A5, Def3; :: thesis: verum