hereby :: thesis: ( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) st
( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` ) implies S is Jordan )

assume A1: S is Jordan ; :: thesis: ( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) st
( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` ) )
hence S ` <> {} ; :: thesis: ex A1, A2 being Subset of (TOP-REAL 2) st
( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` )
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 & C2 is a_component ) by A1;
A6: A2 /\ (S `) = A2 by A2, XBOOLE_1:21;
A1 /\ (S `) = A1 by A2, XBOOLE_1:21;
then reconsider C1 = A1, C2 = A2 as Subset of ((TOP-REAL 2) | (S `)) by A6, TOPS_2:29;
C2 = A2 ;
then A7: C1 is a_component by A5;
take A1 = A1; :: thesis: ex A2 being Subset of (TOP-REAL 2) st
( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` )
take A2 = A2; :: thesis: ( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` )
thus S ` = A1 \/ A2 by A2; :: thesis: ( A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` )
thus A1 misses A2 by A3; :: thesis: ( (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S ` & A2 is_a_component_of S ` )
thus (Cl A1) \ A1 = (Cl A2) \ A2 by A4; :: thesis: ( A1 is_a_component_of S ` & A2 is_a_component_of S ` )
C1 = A1 ;
then C2 is a_component by A5;
hence ( A1 is_a_component_of S ` & A2 is_a_component_of S ` ) by A7, CONNSP_1:def 6; :: thesis: verum

end;

assume A8: S ` <> {} ; :: thesis: ( for A1, A2 being Subset of (TOP-REAL 2) holds
( not S ` = A1 \/ A2 or not A1 misses A2 or not (Cl A1) \ A1 = (Cl A2) \ A2 or not A1 is_a_component_of S ` or not A2 is_a_component_of S ` ) or S is Jordan )
given A1, A2 being Subset of (TOP-REAL 2) such that A9: S ` = A1 \/ A2 and
A10: A1 misses A2 and
A11: (Cl A1) \ A1 = (Cl A2) \ A2 and
A12: A1 is_a_component_of S ` and
A13: A2 is_a_component_of S ` ; :: thesis: S is Jordan
reconsider a1 = A1, a2 = A2 as Subset of (TOP-REAL 2) ;
A14: ex B being Subset of ((TOP-REAL 2) | (S `)) st
( B = a2 & B is a_component ) by A13, CONNSP_1:def 6;
thus S ` <> {} by A8; :: according to JORDAN1:def 2 :: thesis: ex b<sub>1</sub>, b<sub>2</sub> being Element of bool the carrier of (TOP-REAL 2) st
( S ` = b₁ \/ b₂ & b₁ misses b₂ & (Cl b₁) \ b₁ = (Cl b₂) \ b₂ & ( for b₃, b₄ being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b<sub>3</sub> = b<sub>1</sub> or not b<sub>4</sub> = b<sub>2</sub> or ( b<sub>3</sub> is a_component & b<sub>4</sub> is a_component ) ) ) )
take a1 ; :: thesis: ex b<sub>1</sub> being Element of bool the carrier of (TOP-REAL 2) st
( S ` = a1 \/ b₁ & a1 misses b₁ & (Cl a1) \ a1 = (Cl b₁) \ b₁ & ( for b₂, b₃ being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b<sub>2</sub> = a1 or not b<sub>3</sub> = b<sub>1</sub> or ( b<sub>2</sub> is a_component & b<sub>3</sub> is a_component ) ) ) )
take a2 ; :: thesis: ( S ` = a1 \/ a2 & a1 misses a2 & (Cl a1) \ a1 = (Cl a2) \ a2 & ( for b₁, b₂ being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b<sub>1</sub> = a1 or not b<sub>2</sub> = a2 or ( b<sub>1</sub> is a_component & b<sub>2</sub> is a_component ) ) ) )
thus S ` = a1 \/ a2 by A9; :: thesis: ( a1 misses a2 & (Cl a1) \ a1 = (Cl a2) \ a2 & ( for b₁, b₂ being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b<sub>1</sub> = a1 or not b<sub>2</sub> = a2 or ( b<sub>1</sub> is a_component & b<sub>2</sub> is a_component ) ) ) )
thus a1 /\ a2 = {} by A10; :: according to XBOOLE_0:def 7 :: thesis: ( (Cl a1) \ a1 = (Cl a2) \ a2 & ( for b<sub>1</sub>, b<sub>2</sub> being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b₁ = a1 or not b₂ = a2 or ( b₁ is a_component & b₂ is a_component ) ) ) )
thus (Cl a1) \ a1 = (Cl a2) \ a2 by A11; :: thesis: for b₁, b₂ being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b<sub>1</sub> = a1 or not b<sub>2</sub> = a2 or ( b<sub>1</sub> is a_component & b<sub>2</sub> is a_component ) )
ex B being Subset of ((TOP-REAL 2) | (S `)) st
( B = a1 & B is a_component ) by A12, 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 & b₂ is a_component ) ) by A14; :: thesis: verum