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 )
A1: (Cl R) /\ (Cl (R `)) c= Cl (R `) by XBOOLE_1:17;
hereby :: thesis: ( R c= Fr R implies R is boundary )
assume R is boundary ; :: thesis: R c= Fr R
then R ` is dense ;
then (Cl R) /\ (Cl (R `)) = (Cl R) /\ ([#] GX) ;
then Cl R = (Cl R) /\ (Cl (R `)) by XBOOLE_1:28;
hence R c= Fr R by PRE_TOPC:18; :: thesis: verum
end;
A2: R ` c= Cl (R `) by PRE_TOPC:18;
assume R c= Fr R ; :: thesis: R is boundary
then R c= Cl (R `) by A1;
then R \/ (R `) c= Cl (R `) by A2, XBOOLE_1:8;
then [#] GX c= Cl (R `) by PRE_TOPC:2;
then [#] GX = Cl (R `) ;
then R ` is dense ;
hence R is boundary ; :: thesis: verum