let T be non empty TopSpace; :: thesis: for A, B being Subset of T st A is open_condensed & B is open_condensed holds
( Cl A c= Cl B iff A c= B )
let A, B be Subset of T; :: thesis: ( A is open_condensed & B is open_condensed implies ( Cl A c= Cl B iff A c= B ) )
assume that
A1: A is open_condensed and
A2: B is open_condensed ; :: thesis: ( Cl A c= Cl B iff A c= B )
thus ( Cl A c= Cl B implies A c= B ) :: thesis: ( A c= B implies Cl A c= Cl B )
proof
assume Cl A c= Cl B ; :: thesis: A c= B
then A3: Int (Cl A) c= Int (Cl B) by TOPS_1:19;
Int (Cl A) = A by A1, TOPS_1:def 8;
hence A c= B by A2, A3, TOPS_1:def 8; :: thesis: verum
end;
thus ( A c= B implies Cl A c= Cl B ) by PRE_TOPC:19; :: thesis: verum