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 )

proof

assume A is regular_closed ; :: thesis: ( A is subcondensed & A is closed )
then A1: Cl (Int A) = A by TOPS_1:def 7;
then Cl A = A ;
hence ( A is subcondensed & A is closed ) by A1, Def2; :: thesis: verum

end;

assume ( A is subcondensed & A is closed ) ; :: thesis: A is regular_closed
then ( Cl (Int A) = Cl A & Cl A = A ) by Def2, PRE_TOPC:52;
hence A is regular_closed ; :: thesis: verum