let T be TopSpace; :: thesis: for A being Subset of T st A is condensed holds
Cl A is closed_condensed
let A be Subset of T; :: thesis: ( A is condensed implies Cl A is closed_condensed )
assume A1: A is condensed ; :: thesis: Cl A is closed_condensed
then Int (Cl A) c= A by TOPS_1:def 6;
then A2: Cl (Int (Cl A)) c= Cl A by PRE_TOPC:19;
Cl A is condensed by A1, TOPS_1:71;
then Cl A c= Cl (Int (Cl A)) by TOPS_1:def 6;
then Cl A = Cl (Int (Cl A)) by A2;
hence Cl A is closed_condensed by TOPS_1:def 7; :: thesis: verum