let GX be TopStruct ; :: thesis: for R being Subset of GX holds
( R is boundary iff R c= Fr R )
let R be Subset of GX; :: thesis: ( R is boundary iff R c= Fr R )

hereby :: thesis: ( R c= Fr R implies R is boundary )

assume R is boundary ; :: thesis: R c= Fr R
then R ` is dense by Def4;
then (Cl R) /\ (Cl (R ` )) = (Cl R) /\ ([#] GX) by Def3;
then Cl R = (Cl R) /\ (Cl (R ` )) by XBOOLE_1:28;
hence R c= Fr R by PRE_TOPC:48; :: thesis: verum

end;

assume R c= Fr R ; :: thesis: R is boundary
then ( R c= (Cl R) /\ (Cl (R ` )) & (Cl R) /\ (Cl (R ` )) c= Cl (R ` ) ) by XBOOLE_1:17;
then A1: R c= Cl (R ` ) by XBOOLE_1:1;
R ` c= Cl (R ` ) by PRE_TOPC:48;
then R \/ (R ` ) c= Cl (R ` ) by A1, XBOOLE_1:8;
then [#] GX c= Cl (R ` ) by PRE_TOPC:18;
then [#] GX = Cl (R ` ) by XBOOLE_0:def 10;
then R ` is dense by Def3;
hence R is boundary by Def4; :: thesis: verum