let T be non empty TopSpace; :: thesis: for A, B being Subset of T st A is closed_condensed & B is closed_condensed holds
( Int A c= Int B iff A c= B )
let A, B be Subset of T; :: thesis: ( A is closed_condensed & B is closed_condensed implies ( Int A c= Int B iff A c= B ) )
assume that
A1: A is closed_condensed and
A2: B is closed_condensed ; :: thesis: ( Int A c= Int B iff A c= B )
thus ( Int A c= Int B implies A c= B ) :: thesis: ( A c= B implies Int A c= Int B )

proof

assume Int A c= Int B ; :: thesis: A c= B
then A3: Cl (Int A) c= Cl (Int B) by PRE_TOPC:19;
Cl (Int A) = A by A1, TOPS_1:def 7;
hence A c= B by A2, A3, TOPS_1:def 7; :: thesis: verum

end;

thus ( A c= B implies Int A c= Int B ) by TOPS_1:19; :: thesis: verum