let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st n >= 1 & P = {p} holds
P is boundary
let p be Point of (TOP-REAL n); :: thesis: for P being Subset of (TOP-REAL n) st n >= 1 & P = {p} holds
P is boundary
let P be Subset of (TOP-REAL n); :: thesis: ( n >= 1 & P = {p} implies P is boundary )
assume that
A1: n >= 1 and
A2: P = {p} ; :: thesis: P is boundary
the carrier of (TOP-REAL n) c= Cl (P `)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of (TOP-REAL n) or z in Cl (P `) )
assume A3: z in the carrier of (TOP-REAL n) ; :: thesis: z in Cl (P `)

per cases ( z = p or z <> p ) ;

suppose A4: z = p ; :: thesis: z in Cl (P `)

reconsider ez = z as Point of (Euclid n) by A3, TOPREAL3:8;
for G1 being Subset of (TOP-REAL n) st G1 is open & z in G1 holds
P ` meets G1

proof

let G1 be Subset of (TOP-REAL n); :: thesis: ( G1 is open & z in G1 implies P ` meets G1 )
assume A5: G1 is open ; :: thesis: ( not z in G1 or P ` meets G1 )
thus ( z in G1 implies P ` meets G1 ) :: thesis: verum

proof

A6: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider GG = G1 as Subset of (TopSpaceMetr (Euclid n)) ;
assume A7: z in G1 ; :: thesis: P ` meets G1
GG is open by A5, A6, PRE_TOPC:30;
then consider r being Real such that
A8: r > 0 and
A9: Ball (ez,r) c= GG by A7, TOPMETR:15;
reconsider r = r as Real ;
set p2 = p - (((r / 2) / (sqrt n)) * (1.REAL n));
reconsider ep2 = p - (((r / 2) / (sqrt n)) * (1.REAL n)) as Point of (Euclid n) by TOPREAL3:8;
A10: 0 < sqrt n by A1, SQUARE_1:25;
A11: |.(p - (p - (((r / 2) / (sqrt n)) * (1.REAL n)))).| = |.((p - p) + (((r / 2) / (sqrt n)) * (1.REAL n))).| by RLVECT_1:29
.= |.(((((r / 2) / (sqrt n)) * (1.REAL n)) + p) - p).| by RLVECT_1:def 3
.= |.(((r / 2) / (sqrt n)) * (1.REAL n)).| by RLVECT_4:1
.= |.((r / 2) / (sqrt n)).| * |.(1.REAL n).| by TOPRNS_1:7
.= |.((r / 2) / (sqrt n)).| * (sqrt n) by EUCLID:73
.= (|.(r / 2).| / |.(sqrt n).|) * (sqrt n) by COMPLEX1:67
.= (|.(r / 2).| / (sqrt n)) * (sqrt n) by A10, ABSVALUE:def 1
.= |.(r / 2).| by A10, XCMPLX_1:87
.= r / 2 by A8, ABSVALUE:def 1 ;
r / 2 > 0 by A8, XREAL_1:139;
then p <> p - (((r / 2) / (sqrt n)) * (1.REAL n)) by A11, TOPRNS_1:28;
then not p - (((r / 2) / (sqrt n)) * (1.REAL n)) in P by A2, TARSKI:def 1;
then A12: p - (((r / 2) / (sqrt n)) * (1.REAL n)) in P ` by XBOOLE_0:def 5;
r / 2 < r by A8, XREAL_1:216;
then dist (ez,ep2) < r by A4, A11, JGRAPH_1:28;
then p - (((r / 2) / (sqrt n)) * (1.REAL n)) in Ball (ez,r) by METRIC_1:11;
hence P ` meets G1 by A9, A12, XBOOLE_0:3; :: thesis: verum

end;

end;

hence z in Cl (P `) by A3, PRE_TOPC:def 7; :: thesis: verum

end;

suppose z <> p ; :: thesis: z in Cl (P `)

then not z in P by A2, TARSKI:def 1;
then A13: z in P ` by A3, XBOOLE_0:def 5;
P ` c= Cl (P `) by PRE_TOPC:18;
hence z in Cl (P `) by A13; :: thesis: verum

end;

end;

end;

then Cl (P `) = [#] (TOP-REAL n) ;
then P ` is dense by TOPS_1:def 3;
hence P is boundary by TOPS_1:def 4; :: thesis: verum