let C be Simple_closed_curve; :: thesis: ( |[(- 1),0]|,|[1,0]| realize-max-dist-in C implies C is Jordan )
assume A1: |[(- 1),0]|,|[1,0]| realize-max-dist-in C ; :: thesis: C is Jordan
then consider Jc, Jd being compact with_the_max_arc Subset of (TOP-REAL 2) such that
A2: Jc is_an_arc_of |[(- 1),0]|,|[1,0]| and
A3: Jd is_an_arc_of |[(- 1),0]|,|[1,0]| and
A4: C = Jc \/ Jd and
A5: Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} and
A6: UMP C in Jc and
A7: LMP C in Jd and
A8: W-bound C = W-bound Jc and
A9: E-bound C = E-bound Jc by Lm90;
set l = LMP Jc;
set LJ = (LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd;
set k = UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd);
set x = (1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc));
A10: Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) is a_component by CONNSP_1:40;
A11: Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) = BDD C by A1, A2, A3, A4, A5, A6, A7, A8, A9, Th96;
thus C ` <> {} ; :: according to JORDAN1:def 2 :: thesis: ex b<sub>1</sub>, b<sub>2</sub> being Element of bool the carrier of (TOP-REAL 2) st
( C ` = b₁ \/ b₂ & b₁ misses b₂ & (Cl b₁) \ b₁ = (Cl b₂) \ b₂ & ( for b₃, b₄ being Element of bool the carrier of ((TOP-REAL 2) | (C `)) holds
( not b<sub>3</sub> = b<sub>1</sub> or not b<sub>4</sub> = b<sub>2</sub> or ( b<sub>3</sub> is a_component & b<sub>4</sub> is a_component ) ) ) )
take A1 = UBD C; :: thesis: ex b<sub>1</sub> being Element of bool the carrier of (TOP-REAL 2) st
( C ` = A1 \/ b₁ & A1 misses b₁ & (Cl A1) \ A1 = (Cl b₁) \ b₁ & ( for b₂, b₃ being Element of bool the carrier of ((TOP-REAL 2) | (C `)) holds
( not b<sub>2</sub> = A1 or not b<sub>3</sub> = b<sub>1</sub> or ( b<sub>2</sub> is a_component & b<sub>3</sub> is a_component ) ) ) )
take A2 = BDD C; :: thesis: ( C ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & ( for b₁, b₂ being Element of bool the carrier of ((TOP-REAL 2) | (C `)) holds
( not b<sub>1</sub> = A1 or not b<sub>2</sub> = A2 or ( b<sub>1</sub> is a_component & b<sub>2</sub> is a_component ) ) ) )
thus C ` = A1 \/ A2 by JORDAN2C:27; :: thesis: ( A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & ( for b₁, b₂ being Element of bool the carrier of ((TOP-REAL 2) | (C `)) holds
( not b<sub>1</sub> = A1 or not b<sub>2</sub> = A2 or ( b<sub>1</sub> is a_component & b<sub>2</sub> is a_component ) ) ) )
thus A1 misses A2 by JORDAN2C:24; :: thesis: ( (Cl A1) \ A1 = (Cl A2) \ A2 & ( for b<sub>1</sub>, b<sub>2</sub> being Element of bool the carrier of ((TOP-REAL 2) | (C `)) holds
( not b₁ = A1 or not b₂ = A2 or ( b₁ is a_component & b₂ is a_component ) ) ) )
A12: Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) <> {} ((TOP-REAL 2) | (C `)) by A10, CONNSP_1:32;
A1 is_a_component_of C ` by JORDAN2C:124;
then A13: ex B1 being Subset of ((TOP-REAL 2) | (C `)) st
( B1 = A1 & B1 is a_component ) ;
then A14: C = Fr A1 by A11, A12, Lm15
.= (Cl A1) /\ (Cl (A1 `)) ;
A15: C = Fr A2 by A10, A11, A12, Lm15
.= (Cl A2) /\ (Cl (A2 `)) ;
A2 c= C ` by JORDAN2C:25;
then C misses A2 by SUBSET_1:23;
then A16: C c= (Cl A2) \ A2 by A15, XBOOLE_1:17, XBOOLE_1:86;
A17: A1 misses A2 by JORDAN2C:24;
then A2 c= A1 ` by SUBSET_1:23;
then A18: Cl A2 c= A1 ` by TOPS_1:5;
A1 \/ A2 = C ` by JORDAN2C:27;
then A1 \/ A2 misses C by SUBSET_1:23;
then C misses A1 by XBOOLE_1:70;
then A19: A2 \/ C misses A1 by A17, XBOOLE_1:70;
A2 \/ A1 = C ` by JORDAN2C:27;
then (A2 \/ A1) ` misses C ` by SUBSET_1:23;
then ((A2 \/ A1) `) /\ (C `) = {} ;
then ((A2 \/ A1) \/ C) ` = {} by XBOOLE_1:53;
then ((A2 \/ C) \/ A1) ` = {} by XBOOLE_1:4;
then ((A2 \/ C) `) /\ (A1 `) = {} by XBOOLE_1:53;
then (A2 \/ C) ` misses A1 ` ;
then Cl A2 c= A2 \/ C by A18, A19, SUBSET_1:25;
then A20: (Cl A2) \ A2 c= C by XBOOLE_1:43;
A1 c= C ` by JORDAN2C:26;
then C misses A1 by SUBSET_1:23;
then A21: C c= (Cl A1) \ A1 by A14, XBOOLE_1:17, XBOOLE_1:86;
A1 c= A2 ` by A17, SUBSET_1:23;
then A22: Cl A1 c= A2 ` by TOPS_1:5;
A2 \/ A1 = C ` by JORDAN2C:27;
then A2 \/ A1 misses C by SUBSET_1:23;
then C misses A2 by XBOOLE_1:70;
then A23: A1 \/ C misses A2 by A17, XBOOLE_1:70;
A1 \/ A2 = C ` by JORDAN2C:27;
then (A1 \/ A2) ` misses C ` by SUBSET_1:23;
then ((A1 \/ A2) `) /\ (C `) = {} ;
then ((A1 \/ A2) \/ C) ` = {} by XBOOLE_1:53;
then ((A1 \/ C) \/ A2) ` = {} by XBOOLE_1:4;
then ((A1 \/ C) `) /\ (A2 `) = {} by XBOOLE_1:53;
then (A1 \/ C) ` misses A2 ` ;
then Cl A1 c= A1 \/ C by A22, A23, SUBSET_1:25;
then (Cl A1) \ A1 c= C by XBOOLE_1:43;
hence (Cl A1) \ A1 = C by A21
.= (Cl A2) \ A2 by A16, A20 ;
:: thesis: for b₁, b₂ being Element of bool the carrier of ((TOP-REAL 2) | (C `)) holds
( not b<sub>1</sub> = A1 or not b<sub>2</sub> = A2 or ( b<sub>1</sub> is a_component & b<sub>2</sub> is a_component ) )
thus for b<sub>1</sub>, b<sub>2</sub> being Element of bool the carrier of ((TOP-REAL 2) | (C `)) holds
( not b₁ = A1 or not b₂ = A2 or ( b₁ is a_component & b₂ is a_component ) ) by A11, A13, CONNSP_1:40; :: thesis: verum