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 )

proof

assume A is regular_open ; :: thesis: ( A is supercondensed & A is open )
then A1: Int (Cl A) = A by TOPS_1:def 8;
then Int A = A ;
hence ( A is supercondensed & A is open ) by A1, Def1; :: thesis: verum

end;

assume ( A is supercondensed & A is open ) ; :: thesis: A is regular_open
then ( Int (Cl A) = Int A & Int A = A ) by Def1, TOPS_1:55;
hence A is regular_open ; :: thesis: verum