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