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

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

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

end;

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