let C be Simple_closed_curve; :: thesis: ex A1, A2 being Subset of (TOP-REAL 2) st
( C ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (C `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) )
C is Jordan by Lm92;
hence ex A1, A2 being Subset of (TOP-REAL 2) st
( C ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (C `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) ) ; :: thesis: verum