let G be non empty TopSpace; :: thesis: for A being Subset of G st A ` <> {} holds
( A is boundary iff for x being set
for V being Subset of G st x in A & x in V & V is open holds
ex B being Subset of G st
( B is_a_component_of A ` & V meets B ) )
let A be Subset of G; :: thesis: ( A ` <> {} implies ( A is boundary iff for x being set
for V being Subset of G st x in A & x in V & V is open holds
ex B being Subset of G st
( B is_a_component_of A ` & V meets B ) ) )
assume A1: A ` <> {} ; :: thesis: ( A is boundary iff for x being set
for V being Subset of G st x in A & x in V & V is open holds
ex B being Subset of G st
( B is_a_component_of A ` & V meets B ) )

hereby :: thesis: ( ( for x being set
for V being Subset of G st x in A & x in V & V is open holds
ex B being Subset of G st
( B is_a_component_of A ` & V meets B ) ) implies A is boundary )

reconsider A1 = A ` as non empty Subset of G by A1;
reconsider A2 = A ` as Subset of G ;
assume A is boundary ; :: thesis: for x being set
for V being Subset of G st x in A & x in V & V is open holds
ex B being Subset of G st
( B is_a_component_of A ` & V meets B )
then A ` is dense by TOPS_1:def 4;
then A2: Cl (A `) = [#] G by TOPS_1:def 3;
let x be set ; :: thesis: for V being Subset of G st x in A & x in V & V is open holds
ex B being Subset of G st
( B is_a_component_of A ` & V meets B )
let V be Subset of G; :: thesis: ( x in A & x in V & V is open implies ex B being Subset of G st
( B is_a_component_of A ` & V meets B ) )
assume that
x in A and
A3: ( x in V & V is open ) ; :: thesis: ex B being Subset of G st
( B is_a_component_of A ` & V meets B )
A2 meets V by A3, A2, PRE_TOPC:def 7;
then consider z being object such that
A4: z in A ` and
A5: z in V by XBOOLE_0:3;
reconsider p = z as Point of (G | (A `)) by A4, PRE_TOPC:8;
Component_of p c= the carrier of (G | (A `)) ;
then Component_of p c= A ` by PRE_TOPC:8;
then reconsider B0 = Component_of p as Subset of G by XBOOLE_1:1;
A6: not G | A1 is empty ;
then p in Component_of p by CONNSP_1:38;
then p in V /\ B0 by A5, XBOOLE_0:def 4;
then A7: V meets B0 ;
Component_of p is a_component by A6, CONNSP_1:40;
then B0 is_a_component_of A ` by CONNSP_1:def 6;
hence ex B being Subset of G st
( B is_a_component_of A ` & V meets B ) by A7; :: thesis: verum

end;

assume A8: for x being set
for V being Subset of G st x in A & x in V & V is open holds
ex B being Subset of G st
( B is_a_component_of A ` & V meets B ) ; :: thesis: A is boundary
the carrier of G c= Cl (A `)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of G or z in Cl (A `) )
assume A9: z in the carrier of G ; :: thesis: z in Cl (A `)

per cases ( z in A or not z in A ) ;

suppose A10: z in A ; :: thesis: z in Cl (A `)

for G1 being Subset of G st G1 is open & z in G1 holds
A ` meets G1

proof

let G1 be Subset of G; :: thesis: ( G1 is open & z in G1 implies A ` meets G1 )
assume A11: G1 is open ; :: thesis: ( not z in G1 or A ` meets G1 )
assume z in G1 ; :: thesis: A ` meets G1
then consider B being Subset of G such that
A12: B is_a_component_of A ` and
A13: G1 meets B by A8, A10, A11;
A14: G1 /\ B <> {} by A13;
consider B1 being Subset of (G | (A `)) such that
A15: B1 = B and
B1 is a_component by A12, CONNSP_1:def 6;
B1 c= the carrier of (G | (A `)) ;
then B1 c= A ` by PRE_TOPC:8;
then (A `) /\ G1 <> {} G by A15, A14, XBOOLE_1:3, XBOOLE_1:26;
hence A ` meets G1 ; :: thesis: verum

end;

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

end;

suppose A16: not z in A ; :: thesis: z in Cl (A `)

A17: A ` c= Cl (A `) by PRE_TOPC:18;
z in the carrier of G \ A by A9, A16, XBOOLE_0:def 5;
hence z in Cl (A `) by A17; :: thesis: verum

end;

end;

end;

then Cl (A `) = [#] G ;
then A ` is dense by TOPS_1:def 3;
hence A is boundary by TOPS_1:def 4; :: thesis: verum