let n be Element of 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 set ; :: 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:13;
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

assume Z: z in G1 ; :: thesis: P ` meets G1
X: 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)) ;
GG is open by X, A5, PRE_TOPC:60;
then consider r being real number such that
A6: ( r > 0 & Ball ez,r c= GG ) by A5, X, Z, TOPMETR:22;
reconsider r = r as Real by XREAL_0:def 1;
A7: 0 < sqrt n by A1, SQUARE_1:93;
A8: r / 2 > 0 by A6, XREAL_1:141;
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:13;
A9: |.(p - (p - (((r / 2) / (sqrt n)) * (1.REAL n)))).| = |.((p - p) + (((r / 2) / (sqrt n)) * (1.REAL n))).| by EUCLID:51
.= |.(((((r / 2) / (sqrt n)) * (1.REAL n)) + p) - p).| by EUCLID:49
.= |.(((r / 2) / (sqrt n)) * (1.REAL n)).| by EUCLID:52
.= (abs ((r / 2) / (sqrt n))) * |.(1.REAL n).| by TOPRNS_1:8
.= (abs ((r / 2) / (sqrt n))) * (sqrt n) by Th35
.= ((abs (r / 2)) / (abs (sqrt n))) * (sqrt n) by COMPLEX1:153
.= ((abs (r / 2)) / (sqrt n)) * (sqrt n) by A7, ABSVALUE:def 1
.= abs (r / 2) by A7, XCMPLX_1:88
.= r / 2 by A8, ABSVALUE:def 1 ;
r / 2 < r by A6, XREAL_1:218;
then dist ez,ep2 < r by A4, A9, JGRAPH_1:45;
then A10: p - (((r / 2) / (sqrt n)) * (1.REAL n)) in Ball ez,r by METRIC_1:12;
p <> p - (((r / 2) / (sqrt n)) * (1.REAL n)) by A8, A9, TOPRNS_1:29;
then not p - (((r / 2) / (sqrt n)) * (1.REAL n)) in P by A2, TARSKI:def 1;
then p - (((r / 2) / (sqrt n)) * (1.REAL n)) in P ` by XBOOLE_0:def 5;
hence P ` meets G1 by A6, A10, XBOOLE_0:3; :: thesis: verum

end;

end;

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

end;

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

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

end;

end;

end;

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