let T be TopSpace; :: thesis: for A being Subset of T st A is supercondensed holds
A ` is subcondensed
let A be Subset of T; :: thesis: ( A is supercondensed implies A ` is subcondensed )
A1: (Int A) ` = Cl (A ` ) by TDLAT_3:3;
assume A is supercondensed ; :: thesis: A ` is subcondensed
then A2: (Int (Cl A)) ` = (Int A) ` by Def1;
(Int (Cl A)) ` = Cl ((Cl A) ` ) by TDLAT_3:3
.= Cl (Int (A ` )) by TDLAT_3:4 ;
hence A ` is subcondensed by A2, A1, Def2; :: thesis: verum