let T be TopSpace; :: thesis: for A being Subset of T st A is condensed holds
A ` is condensed
let X be Subset of T; :: thesis: ( X is condensed implies X ` is condensed )
assume A1: X is condensed ; :: thesis: X ` is condensed
then X c= Cl (Int X) by TOPS_1:def 6;
then (Cl (((Int X) ` ) ` )) ` c= X ` by SUBSET_1:31;
then Int ((Int X) ` ) c= X ` by TOPS_1:def 1;
then A2: Int (((Cl (X ` )) ` ) ` ) c= X ` by TOPS_1:def 1;
Int (Cl X) c= X by A1, TOPS_1:def 6;
then (Cl ((Cl X) ` )) ` c= X by TOPS_1:def 1;
then X ` c= Cl ((Cl ((X ` ) ` )) ` ) by SUBSET_1:31;
then X ` c= Cl (Int (X ` )) by TOPS_1:def 1;
hence X ` is condensed by A2, TOPS_1:def 6; :: thesis: verum