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

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

assume B is semi-pre-open ; :: thesis: B = spInt B
then B = B /\ ((Cl (Int B)) \/ (Int (Cl B))) by XBOOLE_1:28;
hence B = spInt B by XBOOLE_1:23; :: thesis: verum

end;

assume B = spInt B ; :: thesis: B is semi-pre-open
then B = B /\ ((Cl (Int B)) \/ (Int (Cl B))) by XBOOLE_1:23;
hence B is semi-pre-open by XBOOLE_1:17; :: thesis: verum