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

hereby :: according to SPRECT_1:def 3 :: thesis: ex b₁, b₂ being Element of K24(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 consider s' being Element of (TOP-REAL 2) such that
A5: ( s' in S & f . s = f . s' ) by FUNCT_2:116;
thus contradiction by A2, A5, FUNCT_2:77; :: thesis: verum

end;

take B1 = f .: A1; :: thesis: ex b₁ being Element of K24(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:153;
hence (f .: S) ` = B1 \/ B2 by A3, 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:125; :: 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:74
.= f .: ((Cl A2) \ A2) by A3, FUNCT_1:123
.= (f .: (Cl A2)) \ B2 by FUNCT_1:123
.= (Cl B2) \ B2 by TOPS_2:74 ; :: 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 A4, Th15; :: thesis: verum