let T be TopSpace; :: thesis: for B being Subset of T holds
( B is alpha-set of T iff B = alphaInt B )
let B be Subset of T; :: thesis: ( B is alpha-set of T iff B = alphaInt B )

hereby :: thesis: ( B = alphaInt B implies B is alpha-set of T )

assume B is alpha-set of T ; :: thesis: B = alphaInt B
then B c= Int (Cl (Int B)) by Def1;
hence B = alphaInt B by XBOOLE_1:28; :: thesis: verum

end;

assume B = alphaInt B ; :: thesis: B is alpha-set of T
then B c= Int (Cl (Int B)) by XBOOLE_1:17;
hence B is alpha-set of T by Def1; :: thesis: verum