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:12;
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:12;
then X ` c= Cl (Int (X `)) by TOPS_1:def 1;
hence X ` is condensed by A2, TOPS_1:def 6; :: thesis: verum