let A be Subset of (TOP-REAL 2); :: thesis: ( A ` <> {} implies ( ( A is boundary & A is Jordan ) iff ex A1, A2 being Subset of (TOP-REAL 2) st
( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) ) ) )
assume A1: A ` <> {} ; :: thesis: ( ( A is boundary & A is Jordan ) iff ex A1, A2 being Subset of (TOP-REAL 2) st
( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) ) )

hereby :: thesis: ( ex A1, A2 being Subset of (TOP-REAL 2) st
( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) ) implies ( A is boundary & A is Jordan ) )

assume that
A2: A is boundary and
A3: A is Jordan ; :: thesis: ex A1, A2 being Subset of (TOP-REAL 2) st
( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) )
consider A1, A2 being Subset of (TOP-REAL 2) such that
A4: A ` = A1 \/ A2 and
A5: A1 misses A2 and
A6: (Cl A1) \ A1 = (Cl A2) \ A2 and
A7: for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) by A3, JORDAN1:def 2;
A = (A1 \/ A2) ` by A4;
then A8: A = (A1 `) /\ (A2 `) by XBOOLE_1:53;
A2 c= A ` by A4, XBOOLE_1:7;
then reconsider D2 = A2 as Subset of ((TOP-REAL 2) | (A `)) by PRE_TOPC:8;
A1 c= A ` by A4, XBOOLE_1:7;
then reconsider D1 = A1 as Subset of ((TOP-REAL 2) | (A `)) by PRE_TOPC:8;
D2 = A2 ;
then A9: D1 is a_component by A7;
A10: A c= (Cl A1) \ A1

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in A or z in (Cl A1) \ A1 )
assume A11: z in A ; :: thesis: z in (Cl A1) \ A1
for G being Subset of (TOP-REAL 2) st G is open & z in G holds
A1 \/ A2 meets G

proof

let G be Subset of (TOP-REAL 2); :: thesis: ( G is open & z in G implies A1 \/ A2 meets G )
assume A12: G is open ; :: thesis: ( not z in G or A1 \/ A2 meets G )

hereby :: thesis: verum

assume z in G ; :: thesis: A1 \/ A2 meets G
then consider B being Subset of (TOP-REAL 2) such that
A13: B is_a_component_of A ` and
A14: G meets B by A1, A2, A11, A12, Th81;
consider B1 being Subset of ((TOP-REAL 2) | (A `)) such that
A15: B1 = B and
A16: B1 is a_component by A13, CONNSP_1:def 6;

A17: now :: thesis: ( ( B1 = D1 & B1 c= A1 \/ A2 ) or ( B1,D1 are_separated & B1 c= A1 \/ A2 ) )

per cases ( B1 = D1 or B1,D1 are_separated ) by A9, A16, CONNSP_1:34;

case B1 = D1 ; :: thesis: B1 c= A1 \/ A2

hence B1 c= A1 \/ A2 by XBOOLE_1:7; :: thesis: verum

end;

case B1,D1 are_separated ; :: thesis: B1 c= A1 \/ A2

then A18: ( Cl B1 misses D1 or B1 misses Cl D1 ) by CONNSP_1:def 1;
( B1 is closed & D1 is closed ) by A9, A16, CONNSP_1:33;
then B1 misses D1 by A18, PRE_TOPC:22;
then A19: B1 /\ D1 = {} ;
B1 c= the carrier of ((TOP-REAL 2) | (A `)) ;
then B1 c= A ` by PRE_TOPC:8;
then B1 = B1 /\ (A `) by XBOOLE_1:28
.= (B1 /\ A1) \/ (B1 /\ A2) by A4, XBOOLE_1:23
.= B1 /\ A2 by A19 ;
then A20: B1 c= A2 by XBOOLE_1:17;
A2 c= A1 \/ A2 by XBOOLE_1:7;
hence B1 c= A1 \/ A2 by A20; :: thesis: verum

end;

end;

end;

G /\ B <> {} by A14;
then (A1 \/ A2) /\ G <> {} by A15, A17, XBOOLE_1:3, XBOOLE_1:26;
hence A1 \/ A2 meets G ; :: thesis: verum

end;

end;

then z in Cl (A1 \/ A2) by A11, PRE_TOPC:def 7;
then z in (Cl A1) \/ (Cl A2) by PRE_TOPC:20;
then A21: ( z in Cl A1 or z in Cl A2 ) by XBOOLE_0:def 3;
not z in A ` by A11, XBOOLE_0:def 5;
then ( not z in A1 & not z in A2 ) by A4, XBOOLE_0:def 3;
hence z in (Cl A1) \ A1 by A6, A21, XBOOLE_0:def 5; :: thesis: verum

end;

( (Cl A1) \ A1 c= A1 ` & (Cl A2) \ A2 c= A2 ` ) by XBOOLE_1:33;
then (Cl A1) \ A1 c= A by A6, A8, XBOOLE_1:19;
then A = (Cl A1) \ A1 by A10;
hence ex A1, A2 being Subset of (TOP-REAL 2) st
( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) ) by A4, A5, A6, A7; :: thesis: verum

end;

hereby :: thesis: verum

assume ex A1, A2 being Subset of (TOP-REAL 2) st
( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) ) ; :: thesis: ( A is boundary & A is Jordan )
then consider A1, A2 being Subset of (TOP-REAL 2) such that
A22: A ` = A1 \/ A2 and
A23: ( A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 ) and
A24: A = (Cl A1) \ A1 and
A25: for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ;
for x being set
for V being Subset of (TOP-REAL 2) st x in A & x in V & V is open holds
ex B being Subset of (TOP-REAL 2) st
( B is_a_component_of A ` & V meets B )

proof

A2 c= A ` by A22, XBOOLE_1:7;
then reconsider D2 = A2 as Subset of ((TOP-REAL 2) | (A `)) by PRE_TOPC:8;
A1 c= A ` by A22, XBOOLE_1:7;
then reconsider D1 = A1 as Subset of ((TOP-REAL 2) | (A `)) by PRE_TOPC:8;
let x be set ; :: thesis: for V being Subset of (TOP-REAL 2) st x in A & x in V & V is open holds
ex B being Subset of (TOP-REAL 2) st
( B is_a_component_of A ` & V meets B )
let V be Subset of (TOP-REAL 2); :: thesis: ( x in A & x in V & V is open implies ex B being Subset of (TOP-REAL 2) st
( B is_a_component_of A ` & V meets B ) )
assume that
A26: x in A and
A27: ( x in V & V is open ) ; :: thesis: ex B being Subset of (TOP-REAL 2) st
( B is_a_component_of A ` & V meets B )
D2 = A2 ;
then D1 is a_component by A25;
then A28: A1 is_a_component_of A ` by CONNSP_1:def 6;
x in Cl A1 by A24, A26, XBOOLE_0:def 5;
then A1 meets V by A27, PRE_TOPC:def 7;
hence ex B being Subset of (TOP-REAL 2) st
( B is_a_component_of A ` & V meets B ) by A28; :: thesis: verum

end;

hence ( A is boundary & A is Jordan ) by A1, A22, A23, A25, Th81, JORDAN1:def 2; :: thesis: verum

end;