hereby :: thesis:

assume A1: S is Jordan ; :: thesis:
hence S ` <> {} by JORDAN1:def 2; :: thesis:
consider A1, A2 being Subset of (TOP-REAL 2) such that
A2: S ` = A1 \/ A2 and
A3: A1 misses A2 and
A4: (Cl A1) \ A1 = (Cl A2) \ A2 and
A5: for C1, C2 being Subset of ((TOP-REAL 2) | (S ` )) st C1 = A1 & C2 = A2 holds
( C1 is_a_component_of (TOP-REAL 2) | (S ` ) & C2 is_a_component_of (TOP-REAL 2) | (S ` ) ) by A1, JORDAN1:def 2;
( A1 /\ (S ` ) = A1 & A2 /\ (S ` ) = A2 ) by A2, XBOOLE_1:21;
then reconsider C1 = A1, C2 = A2 as Subset of ((TOP-REAL 2) | (S ` )) by TOPS_2:38;
take A1 = A1; :: thesis:
take A2 = A2; :: thesis:
thus S ` = A1 \/ A2 by A2; :: thesis:
thus A1 misses A2 by A3; :: thesis:
thus (Cl A1) \ A1 = (Cl A2) \ A2 by A4; :: thesis:
( C1 = A1 & C2 = A2 ) ;
then ( C1 is_a_component_of (TOP-REAL 2) | (S ` ) & C2 is_a_component_of (TOP-REAL 2) | (S ` ) ) by A5;
hence ( A1 is_a_component_of S ` & A2 is_a_component_of S ` ) by CONNSP_1:def 6; :: thesis:

end;

assume A6: S ` <> {} ; :: thesis:
given A1, A2 being Subset of (TOP-REAL 2) such that A7: S ` = A1 \/ A2 and
A8: A1 misses A2 and
A9: (Cl A1) \ A1 = (Cl A2) \ A2 and
A10: A1 is_a_component_of S ` and
A11: A2 is_a_component_of S ` ; :: thesis:
thus S ` <> {} by A6; :: according to JORDAN1:def 2 :: thesis:
reconsider a1 = A1, a2 = A2 as Subset of (TOP-REAL 2) ;
take a1 ; :: thesis:
take a2 ; :: thesis:
thus S ` = a1 \/ a2 by A7; :: thesis:
thus a1 /\ a2 = {} by A8, XBOOLE_0:def 7; :: according to XBOOLE_0:def 7 :: thesis:
thus (Cl a1) \ a1 = (Cl a2) \ a2 by A9; :: thesis:
( ex B being Subset of ((TOP-REAL 2) | (S ` )) st
( B = a1 & B is_a_component_of (TOP-REAL 2) | (S ` ) ) & ex B being Subset of ((TOP-REAL 2) | (S ` )) st
( B = a2 & B is_a_component_of (TOP-REAL 2) | (S ` ) ) ) by A10, A11, CONNSP_1:def 6;
hence for b₁, b₂ being Element of bool the carrier of ((TOP-REAL 2) | (S ` )) holds
( not b₁ = a1 or not b₂ = a2 or ( b₁ is_a_component_of (TOP-REAL 2) | (S ` ) & b₂ is_a_component_of (TOP-REAL 2) | (S ` ) ) ) ; :: thesis: