let T be TopSpace; :: thesis: for B being Subset of T holds
( B is semi-open iff B = sInt B )
let B be Subset of T; :: thesis: ( B is semi-open iff B = sInt B )

hereby :: thesis: ( B = sInt B implies B is semi-open )

assume B is semi-open ; :: thesis: B = sInt B
then B c= Cl (Int B) by Def2;
hence B = sInt B by XBOOLE_1:28; :: thesis: verum

end;

assume B = sInt B ; :: thesis: B is semi-open
then B c= Cl (Int B) by XBOOLE_1:17;
hence B is semi-open by Def2; :: thesis: verum