let S be Subset of (TOP-REAL 2); :: thesis: ( S is Jordan implies ( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) ex C1, C2 being Subset of ((TOP-REAL 2) | (S ` )) st
( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & C1 = A1 & C2 = A2 & C1 is_a_component_of (TOP-REAL 2) | (S ` ) & C2 is_a_component_of (TOP-REAL 2) | (S ` ) & ( for C3 being Subset of ((TOP-REAL 2) | (S ` )) holds
( not C3 is_a_component_of (TOP-REAL 2) | (S ` ) or C3 = C1 or C3 = C2 ) ) ) ) )
assume A1: S is Jordan ; :: thesis: ( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) ex C1, C2 being Subset of ((TOP-REAL 2) | (S ` )) st
( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & C1 = A1 & C2 = A2 & C1 is_a_component_of (TOP-REAL 2) | (S ` ) & C2 is_a_component_of (TOP-REAL 2) | (S ` ) & ( for C3 being Subset of ((TOP-REAL 2) | (S ` )) holds
( not C3 is_a_component_of (TOP-REAL 2) | (S ` ) or C3 = C1 or C3 = C2 ) ) ) )
then reconsider S' = S ` as non empty Subset of (TOP-REAL 2) by Def2;
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, Def2;
A6: ( A1 c= S ` & A2 c= S ` ) by A2, XBOOLE_1:7;
A7: [#] ((TOP-REAL 2) | (S ` )) = S ` by PRE_TOPC:def 10;
( A1 c= [#] ((TOP-REAL 2) | (S ` )) & A2 c= [#] ((TOP-REAL 2) | (S ` )) ) by A6, PRE_TOPC:def 10;
then reconsider G0A = A1, G0B = A2 as Subset of ((TOP-REAL 2) | S') ;
( G0A = A1 & G0B = A2 ) ;
then A8: ( G0A is_a_component_of (TOP-REAL 2) | S' & G0B is_a_component_of (TOP-REAL 2) | S' ) by A5;

now

let C3 be Subset of ((TOP-REAL 2) | S'); :: thesis: ( not C3 is_a_component_of (TOP-REAL 2) | S' or C3 = G0A or C3 = G0B )
assume A9: C3 is_a_component_of (TOP-REAL 2) | S' ; :: thesis: ( C3 = G0A or C3 = G0B )
then A10: C3 <> {} ((TOP-REAL 2) | S') by CONNSP_1:34;
C3 /\ (G0A \/ G0B) = C3 by A2, A7, XBOOLE_1:28;
then A11: (C3 /\ G0A) \/ (C3 /\ G0B) <> {} by A10, XBOOLE_1:23;

now

per cases ( C3 /\ G0A <> {} or C3 /\ A2 <> {} ) by A11;

suppose C3 /\ G0A <> {} ; :: thesis: ( C3 = G0A or C3 = G0B )

then A12: C3 meets G0A by XBOOLE_0:def 7;
A13: ( C3 is connected & G0A is connected ) by A8, A9, CONNSP_1:def 5;
then A14: C3 \/ G0A is connected by A12, CONNSP_1:2, CONNSP_1:18;
G0A c= C3 \/ G0A by XBOOLE_1:7;
then G0A = C3 \/ G0A by A8, A14, CONNSP_1:def 5;
then C3 c= G0A by XBOOLE_1:7;
hence ( C3 = G0A or C3 = G0B ) by A9, A13, CONNSP_1:def 5; :: thesis: verum

end;

suppose C3 /\ A2 <> {} ; :: thesis: ( C3 = G0A or C3 = G0B )

then A15: C3 meets G0B by XBOOLE_0:def 7;
A16: ( C3 is connected & G0B is connected ) by A8, A9, CONNSP_1:def 5;
then A17: C3 \/ G0B is connected by A15, CONNSP_1:2, CONNSP_1:18;
G0B c= C3 \/ G0B by XBOOLE_1:7;
then G0B = C3 \/ G0B by A8, A17, CONNSP_1:def 5;
then C3 c= G0B by XBOOLE_1:7;
hence ( C3 = G0A or C3 = G0B ) by A9, A16, CONNSP_1:def 5; :: thesis: verum

end;

end;

end;

hence ( C3 = G0A or C3 = G0B ) ; :: thesis: verum

end;

hence ( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) ex C1, C2 being Subset of ((TOP-REAL 2) | (S ` )) st
( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & C1 = A1 & C2 = A2 & C1 is_a_component_of (TOP-REAL 2) | (S ` ) & C2 is_a_component_of (TOP-REAL 2) | (S ` ) & ( for C3 being Subset of ((TOP-REAL 2) | (S ` )) holds
( not C3 is_a_component_of (TOP-REAL 2) | (S ` ) or C3 = C1 or C3 = C2 ) ) ) ) by A2, A3, A4, A8; :: thesis: verum