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

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

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

end;

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