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

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