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 & C2 is a_component & ( for C3 being Subset of ((TOP-REAL 2) | (S `)) holds
( not C3 is a_component 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 & C2 is a_component & ( for C3 being Subset of ((TOP-REAL 2) | (S `)) holds
( not C3 is a_component or C3 = C1 or C3 = C2 ) ) ) )
then reconsider S9 = S ` as non empty Subset of (TOP-REAL 2) ;
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: A1 c= S ` by A2, XBOOLE_1:7;
A7: A2 c= S ` by A2, XBOOLE_1:7;
A8: [#] ((TOP-REAL 2) | (S `)) = S ` by PRE_TOPC:def 5;
A1 c= [#] ((TOP-REAL 2) | (S `)) by A6, PRE_TOPC:def 5;
then reconsider G0A = A1, G0B = A2 as Subset of ((TOP-REAL 2) | S9) by A7, PRE_TOPC:def 5;
A9: G0A = A1 ;
G0B = A2 ;
then A10: G0A is a_component by A5;
A11: G0B is a_component by A5, A9;

now :: thesis: for C3 being Subset of ((TOP-REAL 2) | S9) holds
( not C3 is a_component or C3 = G0A or C3 = G0B )

let C3 be Subset of ((TOP-REAL 2) | S9); :: thesis: ( not C3 is a_component or C3 = G0A or C3 = G0B )
assume A12: C3 is a_component ; :: thesis: ( C3 = G0A or C3 = G0B )
then A13: C3 <> {} ((TOP-REAL 2) | S9) by CONNSP_1:32;
C3 /\ (G0A \/ G0B) = C3 by A2, A8, XBOOLE_1:28;
then A14: (C3 /\ G0A) \/ (C3 /\ G0B) <> {} by A13, XBOOLE_1:23;

now :: thesis: ( C3 = G0A or C3 = G0B )

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

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

then A15: C3 meets G0A ;
A16: C3 is connected by A12;
A17: G0A is connected by A10;
then A18: C3 \/ G0A is connected by A15, A16, CONNSP_1:1, CONNSP_1:17;
G0A c= C3 \/ G0A by XBOOLE_1:7;
then G0A = C3 \/ G0A by A10, A18;
then C3 c= G0A by XBOOLE_1:7;
hence ( C3 = G0A or C3 = G0B ) by A12, A17; :: thesis: verum

end;

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

then A19: C3 meets G0B ;
A20: C3 is connected by A12;
A21: G0B is connected by A11;
then A22: C3 \/ G0B is connected by A19, A20, CONNSP_1:1, CONNSP_1:17;
G0B c= C3 \/ G0B by XBOOLE_1:7;
then G0B = C3 \/ G0B by A11, A22;
then C3 c= G0B by XBOOLE_1:7;
hence ( C3 = G0A or C3 = G0B ) by A12, A21; :: 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 & C2 is a_component & ( for C3 being Subset of ((TOP-REAL 2) | (S `)) holds
( not C3 is a_component or C3 = C1 or C3 = C2 ) ) ) ) by A2, A3, A4, A10, A11; :: thesis: verum