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

( A is regular_closed iff ( A is subcondensed & A is closed ) )

let A be Subset of T; :: thesis: ( A is regular_closed iff ( A is subcondensed & A is closed ) )

thus ( A is regular_closed implies ( A is subcondensed & A is closed ) ) :: thesis: ( A is subcondensed & A is closed implies A is regular_closed )

A2: A is subcondensed and

A3: A is closed ; :: thesis: A is regular_closed

Cl (Int A) = Cl A by A2;

hence A is regular_closed by A3, PRE_TOPC:22; :: thesis: verum

( A is regular_closed iff ( A is subcondensed & A is closed ) )

let A be Subset of T; :: thesis: ( A is regular_closed iff ( A is subcondensed & A is closed ) )

thus ( A is regular_closed implies ( A is subcondensed & A is closed ) ) :: thesis: ( A is subcondensed & A is closed implies A is regular_closed )

proof

assume that
assume
A is regular_closed
; :: thesis: ( A is subcondensed & A is closed )

then A1: Cl (Int A) = A by TOPS_1:def 7;

thus ( A is subcondensed & A is closed ) by A1; :: thesis: verum

end;then A1: Cl (Int A) = A by TOPS_1:def 7;

thus ( A is subcondensed & A is closed ) by A1; :: thesis: verum

A2: A is subcondensed and

A3: A is closed ; :: thesis: A is regular_closed

Cl (Int A) = Cl A by A2;

hence A is regular_closed by A3, PRE_TOPC:22; :: thesis: verum