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 )
A1: (Cl A) ` = Int (A `) by TDLAT_3:3;
assume A is subcondensed ; :: thesis: A ` is supercondensed
then A2: (Cl (Int A)) ` = (Cl A) ` ;
(Cl (Int A)) ` = Int ((Int A) `) by TDLAT_3:3
.= Int (Cl (A `)) by TDLAT_3:2 ;
hence A ` is supercondensed by A2, A1; :: thesis: verum