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

( A is regular_open iff ( A is supercondensed & A is open ) )

let A be Subset of T; :: thesis: ( A is regular_open iff ( A is supercondensed & A is open ) )

thus ( A is regular_open implies ( A is supercondensed & A is open ) ) :: thesis: ( A is supercondensed & A is open implies A is regular_open )

A2: A is supercondensed and

A3: A is open ; :: thesis: A is regular_open

Int (Cl A) = Int A by A2;

hence A is regular_open by A3, TOPS_1:23; :: thesis: verum

( A is regular_open iff ( A is supercondensed & A is open ) )

let A be Subset of T; :: thesis: ( A is regular_open iff ( A is supercondensed & A is open ) )

thus ( A is regular_open implies ( A is supercondensed & A is open ) ) :: thesis: ( A is supercondensed & A is open implies A is regular_open )

proof

assume that
assume
A is regular_open
; :: thesis: ( A is supercondensed & A is open )

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

thus ( A is supercondensed & A is open ) by A1; :: thesis: verum

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

thus ( A is supercondensed & A is open ) by A1; :: thesis: verum

A2: A is supercondensed and

A3: A is open ; :: thesis: A is regular_open

Int (Cl A) = Int A by A2;

hence A is regular_open by A3, TOPS_1:23; :: thesis: verum