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

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