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 )

assume A2: 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 )
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 A3: ( x in A & x in V & V is open ) ; :: thesis: ex B being Subset of G st
( B is_a_component_of A ` & V meets B )
A ` is dense by A2, TOPS_1:def 4;
then A4: Cl (A ` ) = [#] G by TOPS_1:def 3;
reconsider A2 = A ` as Subset of G ;
A2 meets V by A3, A4, PRE_TOPC:def 13;
then consider z being set such that
A5: ( z in A ` & z in V ) by XBOOLE_0:3;
reconsider p = z as Point of (G | (A ` )) by A5, PRE_TOPC:29;
reconsider A1 = A ` as non empty Subset of G by A1;
A6: not G | A1 is empty ;
then A7: Component_of p is_a_component_of G | (A ` ) by CONNSP_1:43;
Component_of p c= the carrier of (G | (A ` )) ;
then Component_of p c= A ` by PRE_TOPC:29;
then reconsider B0 = Component_of p as Subset of G by XBOOLE_1:1;
A8: B0 is_a_component_of A ` by A7, CONNSP_1:def 6;
p in Component_of p by A6, CONNSP_1:40;
then p in V /\ B0 by A5, XBOOLE_0:def 4;
then V meets B0 by XBOOLE_0:4;
hence ex B being Subset of G st
( B is_a_component_of A ` & V meets B ) by A8; :: thesis: verum

end;

assume A9: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of G or z in Cl (A ` ) )
assume A10: z in the carrier of G ; :: thesis: z in Cl (A ` )

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

suppose A11: 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 A12: 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
A13: ( B is_a_component_of A ` & G1 meets B ) by A9, A11, A12;
consider B1 being Subset of (G | (A ` )) such that
A14: ( B1 = B & B1 is_a_component_of G | (A ` ) ) by A13, CONNSP_1:def 6;
B1 c= the carrier of (G | (A ` )) ;
then A15: B1 c= A ` by PRE_TOPC:29;
G1 /\ B <> {} by A13, XBOOLE_0:def 7;
then (A ` ) /\ G1 <> {} G by A14, A15, XBOOLE_1:3, XBOOLE_1:26;
hence A ` meets G1 by XBOOLE_0:def 7; :: thesis: verum

end;

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

end;

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

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

end;

end;

end;

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