let T be TopSpace; :: thesis: for A being Subset of T st A is condensed holds
Int A is open_condensed
let A be Subset of T; :: thesis: ( A is condensed implies Int A is open_condensed )
assume A1: A is condensed ; :: thesis: Int A is open_condensed
then A c= Cl (Int A) by TOPS_1:def 6;
then A2: Int A c= Int (Cl (Int A)) by TOPS_1:19;
Int A is condensed by A1, TOPS_1:71;
then Int (Cl (Int A)) c= Int A by TOPS_1:def 6;
then Int (Cl (Int A)) = Int A by A2;
hence Int A is open_condensed by TOPS_1:def 8; :: thesis: verum