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

( A is condensed iff ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) )

let A be Subset of T; :: thesis: ( A is condensed iff ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) )

thus ( A is condensed implies ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) ) by Th22; :: thesis: ( Int A is regular_open & Cl A is regular_closed & Border A is empty implies A is condensed )

assume that

A1: Int A is regular_open and

A2: Cl A is regular_closed and

A3: Border A is empty ; :: thesis: A is condensed

A4: A is subcondensed by A2, A3, Th23;

A is supercondensed by A1, A3, Th22;

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

( A is condensed iff ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) )

let A be Subset of T; :: thesis: ( A is condensed iff ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) )

thus ( A is condensed implies ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) ) by Th22; :: thesis: ( Int A is regular_open & Cl A is regular_closed & Border A is empty implies A is condensed )

assume that

A1: Int A is regular_open and

A2: Cl A is regular_closed and

A3: Border A is empty ; :: thesis: A is condensed

A4: A is subcondensed by A2, A3, Th23;

A is supercondensed by A1, A3, Th22;

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