let T be TopSpace; :: thesis: for A being Subset of T holds

( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) )

let A be Subset of T; :: thesis: ( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) )

thus ( A is condensed implies ( Int (Cl A) c= A & A c= Cl (Int A) ) ) by Th8, Th9; :: thesis: ( Int (Cl A) c= A & A c= Cl (Int A) implies A is condensed )

assume that

A1: Int (Cl A) c= A and

A2: A c= Cl (Int A) ; :: thesis: A is condensed

A3: A is subcondensed by A2, Th9;

A is supercondensed by A1, Th8;

hence A is condensed by A3; :: thesis: verum

( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) )

let A be Subset of T; :: thesis: ( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) )

thus ( A is condensed implies ( Int (Cl A) c= A & A c= Cl (Int A) ) ) by Th8, Th9; :: thesis: ( Int (Cl A) c= A & A c= Cl (Int A) implies A is condensed )

assume that

A1: Int (Cl A) c= A and

A2: A c= Cl (Int A) ; :: thesis: A is condensed

A3: A is subcondensed by A2, Th9;

A is supercondensed by A1, Th8;

hence A is condensed by A3; :: thesis: verum