let GX be non empty TopSpace; :: thesis: for R being Subset of GX
for p being Point of GX holds
( p in Cl R iff for T being Subset of GX st T is open & p in T holds
R meets T )
let R be Subset of GX; :: thesis: for p being Point of GX holds
( p in Cl R iff for T being Subset of GX st T is open & p in T holds
R meets T )
let p be Point of GX; :: thesis: ( p in Cl R iff for T being Subset of GX st T is open & p in T holds
R meets T )
hereby :: thesis: ( ( for T being Subset of GX st T is open & p in T holds
R meets T ) implies p in Cl R )
assume A1: p in Cl R ; :: thesis: for T being Subset of GX holds
( not T is open or not p in T or not R misses T )
given T being Subset of GX such that A2: T is open and
A3: p in T and
A4: R misses T ; :: thesis: contradiction
A5: (R `) \/ (T `) = (R /\ T) ` by XBOOLE_1:54;
A6: R /\ T = {} GX by A4;
A7: R c= T `
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in T ` )
assume A8: x in R ; :: thesis: x in T `
then ( x in R ` or x in T ` ) by A5, A6, XBOOLE_0:def 3;
hence x in T ` by A8, XBOOLE_0:def 5; :: thesis: verum
end;
Cl (T `) = T ` by A2, PRE_TOPC:22;
then Cl R c= T ` by A7, PRE_TOPC:19;
hence contradiction by A1, A3, XBOOLE_0:def 5; :: thesis: verum
end;
assume A9: for T being Subset of GX st T is open & p in T holds
R meets T ; :: thesis: p in Cl R
assume not p in Cl R ; :: thesis: contradiction
then p in (Cl R) ` by SUBSET_1:29;
then A10: R meets (Cl R) ` by A9;
R misses R ` by XBOOLE_1:79;
then A11: R /\ (R `) = {} ;
R c= Cl R by PRE_TOPC:18;
then (Cl R) ` c= R ` by SUBSET_1:12;
then R /\ ((Cl R) `) = {} by A11, XBOOLE_1:3, XBOOLE_1:26;
hence contradiction by A10; :: thesis: verum