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

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