let GX be non empty TopSpace; :: thesis: for R being Subset of GX
for p being Point of GX holds
( p in Fr R iff for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S ) )
let R be Subset of GX; :: thesis: for p being Point of GX holds
( p in Fr R iff for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S ) )
let p be Point of GX; :: thesis: ( p in Fr R iff for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S ) )
hereby :: thesis: ( ( for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S ) ) implies p in Fr R )
assume A1: p in Fr R ; :: thesis: for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S )
then A2: p in Cl (R `) by XBOOLE_0:def 4;
let S be Subset of GX; :: thesis: ( S is open & p in S implies ( R meets S & R ` meets S ) )
assume that
A3: S is open and
A4: p in S ; :: thesis: ( R meets S & R ` meets S )
p in Cl R by A1, XBOOLE_0:def 4;
hence ( R meets S & R ` meets S ) by A3, A4, A2, Th12; :: thesis: verum
end;
assume A5: for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S ) ; :: thesis: p in Fr R
then for S being Subset of GX st S is open & p in S holds
R ` meets S ;
then A6: p in Cl (R `) by Th12;
for S being Subset of GX st S is open & p in S holds
R meets S by A5;
then p in Cl R by Th12;
hence p in Fr R by A6, XBOOLE_0:def 4; :: thesis: verum