theorem :: JORDAN1:42

for S being Subset of (TOP-REAL 2) st S is Jordan holds
( 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 ) ) ) )