thus ( A is condensed implies ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) ) by TDLAT_3:9; :: thesis: ( Cl (Int A) = Cl A & Int (Cl A) = Int A implies A is condensed )
assume that
A1: Cl (Int A) = Cl A and
A2: Int (Cl A) = Int A ; :: thesis: A is condensed
A3: Int A c= A by TOPS_1:16;
A c= Cl (Int A) by A1, PRE_TOPC:18;
hence A is condensed by A2, A3, TOPS_1:def 6; :: thesis: verum