let GX be TopStruct ; :: thesis: for R being Subset of GX holds
( R is boundary iff Int R = {} )
let R be Subset of GX; :: thesis: ( R is boundary iff Int R = {} )
( R is boundary iff R ` is dense ) ;
then ( R is boundary iff Cl (R `) = [#] GX ) ;
then ( R is boundary iff (Cl (R `)) ` = ([#] GX) ` ) by SUBSET_1:42;
hence ( R is boundary iff Int R = {} ) by XBOOLE_1:37; :: thesis: verum