let S be Subset of (TOP-REAL 2); :: thesis: for f being Homeomorphism of TOP-REAL 2 st S is Jordan holds
f .: S is Jordan
let f be Homeomorphism of TOP-REAL 2; :: thesis: ( S is Jordan implies f .: S is Jordan )
set s = the Element of S ` ;
assume A1: S ` <> {} ; :: according to SPRECT_1:def 3 :: thesis: ( for b₁, b₂ being Element of K16( the carrier of (TOP-REAL 2)) holds
( not S ` = b<sub>1</sub> \/ b<sub>2</sub> or not b<sub>1</sub> misses b<sub>2</sub> or not (Cl b<sub>1</sub>) \ b<sub>1</sub> = (Cl b<sub>2</sub>) \ b<sub>2</sub> or not b<sub>1</sub> is_a_component_of S ` or not b₂ is_a_component_of S ` ) or f .: S is Jordan )
then the Element of S ` in S ` ;
then reconsider s = the Element of S ` as Element of (TOP-REAL 2) ;
given 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: ( A1 is_a_component_of S ` & A2 is_a_component_of S ` ) ; :: thesis: f .: S is Jordan
A6: not s in S by A1, XBOOLE_0:def 5;

hereby :: according to SPRECT_1:def 3 :: thesis: ex b₁, b₂ being Element of K16( the carrier of (TOP-REAL 2)) st
( (f .: S) ` = b<sub>1</sub> \/ b<sub>2</sub> & b<sub>1</sub> misses b<sub>2</sub> & (Cl b<sub>1</sub>) \ b<sub>1</sub> = (Cl b<sub>2</sub>) \ b<sub>2</sub> & b<sub>1</sub> is_a_component_of (f .: S) ` & b₂ is_a_component_of (f .: S) ` )

assume (f .: S) ` = {} ; :: thesis: contradiction
then f .: S = the carrier of (TOP-REAL 2) by Th9;
then ex s9 being Element of (TOP-REAL 2) st
( s9 in S & f . s = f . s9 ) by FUNCT_2:65;
hence contradiction by A6, FUNCT_2:56; :: thesis: verum

end;

take B1 = f .: A1; :: thesis: ex b₁ being Element of K16( the carrier of (TOP-REAL 2)) st
( (f .: S) ` = B1 \/ b<sub>1</sub> & B1 misses b<sub>1</sub> & (Cl B1) \ B1 = (Cl b<sub>1</sub>) \ b<sub>1</sub> & B1 is_a_component_of (f .: S) ` & b₁ is_a_component_of (f .: S) ` )
take B2 = f .: A2; :: thesis: ( (f .: S) ` = B1 \/ B2 & B1 misses B2 & (Cl B1) \ B1 = (Cl B2) \ B2 & B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` )
f .: (A1 \/ A2) = B1 \/ B2 by RELAT_1:120;
hence (f .: S) ` = B1 \/ B2 by A2, JORDAN1K:5; :: thesis: ( B1 misses B2 & (Cl B1) \ B1 = (Cl B2) \ B2 & B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` )
thus B1 misses B2 by A3, FUNCT_1:66; :: thesis: ( (Cl B1) \ B1 = (Cl B2) \ B2 & B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` )
thus (Cl B1) \ B1 = (f .: (Cl A1)) \ B1 by TOPS_2:60
.= f .: ((Cl A2) \ A2) by A4, FUNCT_1:64
.= (f .: (Cl A2)) \ B2 by FUNCT_1:64
.= (Cl B2) \ B2 by TOPS_2:60 ; :: thesis: ( B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` )
f .: (S `) = (f .: S) ` by JORDAN1K:5;
hence ( B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` ) by A5, Th15; :: thesis: verum