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