jordan1j.miz

begin

 reserve n for Nat;

 theorem :: JORDAN1J:1



 Th1: for G be Go-board holds for i1,i2,j1,j2 be Nat st 1 <= j1 & j1 <= ( width G) & 1 <= j2 & j2 <= ( width G) & 1 <= i1 & i1 < i2 & i2 <= ( len G) holds ((G * (i1,j1)) `1 ) < ((G * (i2,j2)) `1 )

 proof

 let G be Go-board;

 let i1,i2,j1,j2 be Nat;

 assume that

 A1: 1 <= j1 and

 A2: j1 <= ( width G) and

 A3: 1 <= j2 and

 A4: j2 <= ( width G) and

 A5: 1 <= i1 and

 A6: i1 < i2 and

 A7: i2 <= ( len G);



 A8: 1 <= i2 by A5, A6, XXREAL_0: 2;



 then ((G * (i2,j1)) `1 ) = ((G * (i2,1)) `1 ) by A1, A2, A7, GOBOARD5: 2

 .= ((G * (i2,j2)) `1 ) by A3, A4, A7, A8, GOBOARD5: 2;

 hence thesis by A1, A2, A5, A6, A7, GOBOARD5: 3;

 end;

 theorem :: JORDAN1J:2



 Th2: for G be Go-board holds for i1,i2,j1,j2 be Nat st 1 <= i1 & i1 <= ( len G) & 1 <= i2 & i2 <= ( len G) & 1 <= j1 & j1 < j2 & j2 <= ( width G) holds ((G * (i1,j1)) `2 ) < ((G * (i2,j2)) `2 )

 proof

 let G be Go-board;

 let i1,i2,j1,j2 be Nat;

 assume that

 A1: 1 <= i1 and

 A2: i1 <= ( len G) and

 A3: 1 <= i2 and

 A4: i2 <= ( len G) and

 A5: 1 <= j1 and

 A6: j1 < j2 and

 A7: j2 <= ( width G);



 A8: 1 <= j2 by A5, A6, XXREAL_0: 2;



 then ((G * (i1,j2)) `2 ) = ((G * (1,j2)) `2 ) by A1, A2, A7, GOBOARD5: 1

 .= ((G * (i2,j2)) `2 ) by A3, A4, A7, A8, GOBOARD5: 1;

 hence thesis by A1, A2, A5, A6, A7, GOBOARD5: 4;

 end;

 registration

 let f be non empty FinSequence;

 let g be FinSequence;

 cluster (f ^' g) -> non empty;

 coherence

 proof

 (f ^' g) = (f ^ ((2,( len g)) -cut g)) by FINSEQ_6:def 5;

 hence thesis;

 end;

 end

 theorem :: JORDAN1J:3



 Th3: for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds for n be Nat holds (( L~ (( Cage (C,n)) -: ( E-max ( L~ ( Cage (C,n)))))) /\ ( L~ (( Cage (C,n)) :- ( E-max ( L~ ( Cage (C,n))))))) = {( N-min ( L~ ( Cage (C,n)))), ( E-max ( L~ ( Cage (C,n))))}

 proof

 let C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2);

 let n be Nat;

 set US = (( Cage (C,n)) -: ( E-max ( L~ ( Cage (C,n)))));

 set LS = (( Cage (C,n)) :- ( E-max ( L~ ( Cage (C,n)))));

 set f = ( Cage (C,n));

 set pW = ( E-max ( L~ ( Cage (C,n))));

 set pN = ( N-min ( L~ ( Cage (C,n))));



 A1: (pW `1 ) = ( E-bound ( L~ f)) by EUCLID: 52;



 A2: pW in ( rng ( Cage (C,n))) by SPRECT_2: 46;

 then

 A3: (( Cage (C,n)) -: pW) <> {} by FINSEQ_5: 47;

 ((( Cage (C,n)) :- pW) /. 1) = pW by FINSEQ_5: 53;

 then

 A4: ( E-max ( L~ ( Cage (C,n)))) in ( rng (( Cage (C,n)) :- ( E-max ( L~ ( Cage (C,n)))))) by FINSEQ_6: 42;

 ((f :- pW) /. ( len (f :- pW))) = (f /. ( len f)) by A2, FINSEQ_5: 54

 .= (f /. 1) by FINSEQ_6:def 1

 .= pN by JORDAN9: 32;

 then

 A5: pN in ( rng (( Cage (C,n)) :- pW)) by FINSEQ_6: 168;

 {pN, pW} c= ( rng LS) by A5, A4, TARSKI:def 2;

 then

 A6: ( card {pN, pW}) c= ( card ( rng LS)) by CARD_1: 11;

 ( card ( rng LS)) c= ( card ( dom LS)) by CARD_2: 61;

 then

 A7: ( card ( rng LS)) c= ( len LS) by CARD_1: 62;

 ( N-max ( L~ f)) in ( L~ f) by SPRECT_1: 11;

 then (( N-max ( L~ f)) `1 ) <= (pW `1 ) by A1, PSCOMP_1: 24;

 then

 A8: pN <> pW by SPRECT_2: 51;

 then ( card {pN, pW}) = 2 by CARD_2: 57;

 then ( Segm 2) c= ( Segm ( len LS)) by A6, A7;

 then ( len LS) >= 2 by NAT_1: 39;

 then

 A9: ( rng LS) c= ( L~ LS) by SPPOL_2: 18;

 ( len (f -: pW)) = (pW .. f) by A2, FINSEQ_5: 42;

 then ((f -: pW) /. ( len (f -: pW))) = pW by A2, FINSEQ_5: 45;

 then

 A10: pW in ( rng (( Cage (C,n)) -: pW)) by A3, FINSEQ_6: 168;

 ((( Cage (C,n)) -: pW) /. 1) = (( Cage (C,n)) /. 1) by A2, FINSEQ_5: 44

 .= pN by JORDAN9: 32;

 then

 A11: ( N-min ( L~ ( Cage (C,n)))) in ( rng (( Cage (C,n)) -: ( E-max ( L~ ( Cage (C,n)))))) by A3, FINSEQ_6: 42;

 {pN, pW} c= ( rng US) by A11, A10, TARSKI:def 2;

 then

 A12: ( card {pN, pW}) c= ( card ( rng US)) by CARD_1: 11;

 ( card ( rng US)) c= ( card ( dom US)) by CARD_2: 61;

 then

 A13: ( card ( rng US)) c= ( len US) by CARD_1: 62;

 (LS /. ( len LS)) = (( Cage (C,n)) /. ( len ( Cage (C,n)))) by A2, FINSEQ_5: 54

 .= (( Cage (C,n)) /. 1) by FINSEQ_6:def 1

 .= ( N-min ( L~ ( Cage (C,n)))) by JORDAN9: 32;

 then

 A14: ( N-min ( L~ ( Cage (C,n)))) in ( rng LS) by FINSEQ_6: 168;

 (pW .. ( Cage (C,n))) <= (pW .. ( Cage (C,n)));

 then

 A15: ( E-max ( L~ ( Cage (C,n)))) in ( rng US) by A2, FINSEQ_5: 46;

 ( card {pN, pW}) = 2 by A8, CARD_2: 57;

 then

 A16: ( Segm 2) c= ( Segm ( len US)) by A12, A13;

 then

 A17: ( len US) >= 2 by NAT_1: 39;

 then

 A18: ( rng US) c= ( L~ US) by SPPOL_2: 18;

 thus (( L~ US) /\ ( L~ LS)) c= {( N-min ( L~ ( Cage (C,n)))), ( E-max ( L~ ( Cage (C,n))))}

 proof

 let x be object;

 assume

 A19: x in (( L~ US) /\ ( L~ LS));

 then

 reconsider x1 = x as Point of ( TOP-REAL 2);

 assume

 A20: not x in {( N-min ( L~ ( Cage (C,n)))), ( E-max ( L~ ( Cage (C,n))))};

 x in ( L~ US) by A19, XBOOLE_0:def 4;

 then

 consider i1 be Nat such that

 A21: 1 <= i1 and

 A22: (i1 + 1) <= ( len US) and

 A23: x1 in ( LSeg (US,i1)) by SPPOL_2: 13;



 A24: ( LSeg (US,i1)) = ( LSeg (f,i1)) by A22, SPPOL_2: 9;

 x in ( L~ LS) by A19, XBOOLE_0:def 4;

 then

 consider i2 be Nat such that

 A25: 1 <= i2 and

 A26: (i2 + 1) <= ( len LS) and

 A27: x1 in ( LSeg (LS,i2)) by SPPOL_2: 13;

 set i3 = (i2 -' 1);



 A28: (i3 + 1) = i2 by A25, XREAL_1: 235;

 then

 A29: (1 + (pW .. f)) <= ((i3 + 1) + (pW .. f)) by A25, XREAL_1: 7;



 A30: ( len LS) = ((( len f) - (pW .. f)) + 1) by A2, FINSEQ_5: 50;

 then i2 < ((( len f) - (pW .. f)) + 1) by A26, NAT_1: 13;

 then (i2 - 1) < (( len f) - (pW .. f)) by XREAL_1: 19;

 then

 A31: ((i2 - 1) + (pW .. f)) < ( len f) by XREAL_1: 20;

 (i2 - 1) >= (1 - 1) by A25, XREAL_1: 9;

 then

 A32: (i3 + (pW .. f)) < ( len f) by A31, XREAL_0:def 2;



 A33: ( LSeg (LS,i2)) = ( LSeg (f,(i3 + (pW .. f)))) by A2, A28, SPPOL_2: 10;



 A34: ( len US) = (pW .. f) by A2, FINSEQ_5: 42;

 then (i1 + 1) < ((pW .. f) + 1) by A22, NAT_1: 13;

 then (i1 + 1) < ((i3 + (pW .. f)) + 1) by A29, XXREAL_0: 2;

 then

 A35: (i1 + 1) <= (i3 + (pW .. f)) by NAT_1: 13;



 A36: (((pW .. f) -' 1) + 1) = (pW .. f) by A2, FINSEQ_4: 21, XREAL_1: 235;

 (i3 + 1) < ((( len f) - (pW .. f)) + 1) by A26, A28, A30, NAT_1: 13;

 then i3 < (( len f) - (pW .. f)) by XREAL_1: 7;

 then

 A37: (i3 + (pW .. f)) < ( len f) by XREAL_1: 20;

 then

 A38: ((i3 + (pW .. f)) + 1) <= ( len f) by NAT_1: 13;

 now

 per cases by A21, A35, XXREAL_0: 1;

 suppose (i1 + 1) < (i3 + (pW .. f)) & i1 > 1;

 then ( LSeg (f,i1)) misses ( LSeg (f,(i3 + (pW .. f)))) by A37, GOBOARD5:def 4;

 then (( LSeg (f,i1)) /\ ( LSeg (f,(i3 + (pW .. f))))) = {} ;

 hence contradiction by A23, A27, A24, A33, XBOOLE_0:def 4;

 end;

 suppose

 A39: i1 = 1;



 A40: (i3 + (pW .. f)) >= ( 0 + 2) by A17, A34, XREAL_1: 7;

 now

 per cases by A40, XXREAL_0: 1;

 suppose (i3 + (pW .. f)) > 2;

 then

 A41: (i1 + 1) < (i3 + (pW .. f)) by A39;

 now

 per cases by A38, XXREAL_0: 1;

 suppose ((i3 + (pW .. f)) + 1) < ( len f);

 then ( LSeg (f,i1)) misses ( LSeg (f,(i3 + (pW .. f)))) by A41, GOBOARD5:def 4;

 then (( LSeg (f,i1)) /\ ( LSeg (f,(i3 + (pW .. f))))) = {} ;

 hence contradiction by A23, A27, A24, A33, XBOOLE_0:def 4;

 end;

 suppose ((i3 + (pW .. f)) + 1) = ( len f);

 then (i3 + (pW .. f)) = (( len f) - 1);

 then (i3 + (pW .. f)) = (( len f) -' 1) by XREAL_0:def 2;

 then (( LSeg (f,i1)) /\ ( LSeg (f,(i3 + (pW .. f))))) = {(f /. 1)} by A39, GOBOARD7: 34, REVROT_1: 30;

 then x1 in {(f /. 1)} by A23, A27, A24, A33, XBOOLE_0:def 4;



 then x1 = (f /. 1) by TARSKI:def 1

 .= pN by JORDAN9: 32;

 hence contradiction by A20, TARSKI:def 2;

 end;

 end;

 hence contradiction;

 end;

 suppose

 A42: (i3 + (pW .. f)) = 2;



 A43: (1 + 2) <= ( len f) by GOBOARD7: 34, XXREAL_0: 2;

 x1 in (( LSeg (f,1)) /\ ( LSeg (f,(1 + 1)))) by A23, A27, A24, A33, A39, A42, XBOOLE_0:def 4;

 then x1 in {(f /. (1 + 1))} by A43, TOPREAL1:def 6;

 then

 A44: x1 = (f /. (1 + 1)) by TARSKI:def 1;

 ( 0 + (pW .. f)) >= (i3 + (pW .. f)) by A16, A34, A42, NAT_1: 39;

 then

 A45: i3 = 0 by XREAL_1: 6;

 ( 0 + 1) in ( dom LS) by FINSEQ_5: 6;

 then (LS /. 1) = x1 by A2, A42, A44, A45, FINSEQ_5: 52;

 then x1 = pW by FINSEQ_5: 53;

 hence contradiction by A20, TARSKI:def 2;

 end;

 end;

 hence contradiction;

 end;

 suppose

 A46: (i1 + 1) = (i3 + (pW .. f));

 (i3 + (pW .. f)) >= (pW .. f) by NAT_1: 11;

 then (pW .. f) < ( len f) by A32, XXREAL_0: 2;

 then ((pW .. f) + 1) <= ( len f) by NAT_1: 13;

 then

 A47: (((pW .. f) -' 1) + (1 + 1)) <= ( len f) by A36;

 ( 0 + (pW .. f)) <= (i3 + (pW .. f)) by XREAL_1: 7;

 then (pW .. f) = (i1 + 1) by A22, A34, A46, XXREAL_0: 1;

 then (( LSeg (f,i1)) /\ ( LSeg (f,(i3 + (pW .. f))))) = {(f /. (pW .. f))} by A21, A36, A46, A47, TOPREAL1:def 6;

 then x1 in {(f /. (pW .. f))} by A23, A27, A24, A33, XBOOLE_0:def 4;



 then x1 = (f /. (pW .. f)) by TARSKI:def 1

 .= pW by A2, FINSEQ_5: 38;

 hence contradiction by A20, TARSKI:def 2;

 end;

 end;

 hence contradiction;

 end;



 A48: (US /. 1) = (( Cage (C,n)) /. 1) by A2, FINSEQ_5: 44

 .= ( N-min ( L~ ( Cage (C,n)))) by JORDAN9: 32;

 US is non empty by A16, NAT_1: 39;

 then

 A49: ( N-min ( L~ ( Cage (C,n)))) in ( rng US) by A48, FINSEQ_6: 42;



 A50: ( E-max ( L~ ( Cage (C,n)))) in ( rng LS) by FINSEQ_6: 61;

 thus {( N-min ( L~ ( Cage (C,n)))), ( E-max ( L~ ( Cage (C,n))))} c= (( L~ US) /\ ( L~ LS))

 proof

 let x be object;

 assume

 A51: x in {( N-min ( L~ ( Cage (C,n)))), ( E-max ( L~ ( Cage (C,n))))};

 per cases by A51, TARSKI:def 2;

 suppose x = ( N-min ( L~ ( Cage (C,n))));

 hence thesis by A9, A18, A49, A14, XBOOLE_0:def 4;

 end;

 suppose x = ( E-max ( L~ ( Cage (C,n))));

 hence thesis by A9, A50, A18, A15, XBOOLE_0:def 4;

 end;

 end;

 end;

 theorem :: JORDAN1J:4



 Th4: for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds ( Upper_Seq (C,n)) = (( Rotate (( Cage (C,n)),( E-max ( L~ ( Cage (C,n)))))) :- ( W-min ( L~ ( Cage (C,n)))))

 proof

 let C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2);

 set Nmi = ( N-min ( L~ ( Cage (C,n))));

 set Nma = ( N-max ( L~ ( Cage (C,n))));

 set Wmi = ( W-min ( L~ ( Cage (C,n))));

 set Wma = ( W-max ( L~ ( Cage (C,n))));

 set Ema = ( E-max ( L~ ( Cage (C,n))));

 set Emi = ( E-min ( L~ ( Cage (C,n))));

 set Sma = ( S-max ( L~ ( Cage (C,n))));

 set Smi = ( S-min ( L~ ( Cage (C,n))));

 set RotWmi = ( Rotate (( Cage (C,n)),Wmi));

 set RotEma = ( Rotate (( Cage (C,n)),Ema));



 A1: Nmi in ( rng ( Cage (C,n))) by SPRECT_2: 39;



 A2: (( Cage (C,n)) /. 1) = Nmi by JORDAN9: 32;

 then (Emi .. ( Cage (C,n))) <= (Sma .. ( Cage (C,n))) by SPRECT_2: 72;

 then (Ema .. ( Cage (C,n))) < (Sma .. ( Cage (C,n))) by A2, SPRECT_2: 71, XXREAL_0: 2;

 then

 A3: (Ema .. ( Cage (C,n))) < (Smi .. ( Cage (C,n))) by A2, SPRECT_2: 73, XXREAL_0: 2;

 then

 A4: (Ema .. ( Cage (C,n))) < (Wmi .. ( Cage (C,n))) by A2, SPRECT_2: 74, XXREAL_0: 2;

 ((( Cage (C,n)) :- Ema) /. 1) = Ema by FINSEQ_5: 53;

 then

 A5: Ema in ( rng (( Cage (C,n)) :- Ema)) by FINSEQ_6: 42;



 A6: Ema in ( rng ( Cage (C,n))) by SPRECT_2: 46;



 then ((( Cage (C,n)) :- Ema) /. ( len (( Cage (C,n)) :- Ema))) = (( Cage (C,n)) /. ( len ( Cage (C,n)))) by FINSEQ_5: 54

 .= (( Cage (C,n)) /. 1) by FINSEQ_6:def 1

 .= Nmi by JORDAN9: 32;

 then

 A7: Nmi in ( rng (( Cage (C,n)) :- Ema)) by FINSEQ_6: 168;

 {Nmi, Ema} c= ( rng (( Cage (C,n)) :- Ema)) by A7, A5, TARSKI:def 2;

 then

 A8: ( card {Nmi, Ema}) c= ( card ( rng (( Cage (C,n)) :- Ema))) by CARD_1: 11;



 A9: Wmi in ( rng ( Cage (C,n))) by SPRECT_2: 43;

 then

 A10: (( Cage (C,n)) -: Wmi) <> {} by FINSEQ_5: 47;

 ( len (( Cage (C,n)) -: Wmi)) = (Wmi .. ( Cage (C,n))) by A9, FINSEQ_5: 42;

 then ((( Cage (C,n)) -: Wmi) /. ( len (( Cage (C,n)) -: Wmi))) = Wmi by A9, FINSEQ_5: 45;

 then

 A11: Wmi in ( rng (( Cage (C,n)) -: Wmi)) by A10, FINSEQ_6: 168;

 ((( Cage (C,n)) -: Wmi) /. 1) = (( Cage (C,n)) /. 1) by A9, FINSEQ_5: 44

 .= Nmi by JORDAN9: 32;

 then

 A12: Nmi in ( rng (( Cage (C,n)) -: Wmi)) by A10, FINSEQ_6: 42;

 {Nmi, Wmi} c= ( rng (( Cage (C,n)) -: Wmi)) by A12, A11, TARSKI:def 2;

 then

 A13: ( card {Nmi, Wmi}) c= ( card ( rng (( Cage (C,n)) -: Wmi))) by CARD_1: 11;

 ( card ( rng (( Cage (C,n)) -: Wmi))) c= ( card ( dom (( Cage (C,n)) -: Wmi))) by CARD_2: 61;

 then

 A14: ( card ( rng (( Cage (C,n)) -: Wmi))) c= ( len (( Cage (C,n)) -: Wmi)) by CARD_1: 62;



 A15: (Nmi `2 ) = ( N-bound ( L~ ( Cage (C,n)))) by EUCLID: 52;

 (Nma `1 ) <= (( NE-corner ( L~ ( Cage (C,n)))) `1 ) by PSCOMP_1: 38;

 then

 A16: (Nma `1 ) <= ( E-bound ( L~ ( Cage (C,n)))) by EUCLID: 52;

 (Nmi `1 ) < (Nma `1 ) by SPRECT_2: 51;

 then

 A17: Nmi <> Ema by A16, EUCLID: 52;

 then

 A18: ( card {Nmi, Ema}) = 2 by CARD_2: 57;



 A19: (Smi .. ( Cage (C,n))) <= (Wmi .. ( Cage (C,n))) by A2, SPRECT_2: 74;

 then

 A20: Ema in ( rng (( Cage (C,n)) -: Wmi)) by A9, A6, A3, FINSEQ_5: 46, XXREAL_0: 2;



 A21: Wmi in ( rng (( Cage (C,n)) :- Ema)) by A9, A6, A19, A3, FINSEQ_6: 62, XXREAL_0: 2;

 Wma in ( L~ ( Cage (C,n))) by SPRECT_1: 13;

 then (Wma `2 ) <= (Nmi `2 ) by A15, PSCOMP_1: 24;

 then

 A22: Nmi <> Wmi by SPRECT_2: 57;

 then ( card {Nmi, Wmi}) = 2 by CARD_2: 57;

 then ( Segm 2) c= ( Segm ( len (( Cage (C,n)) -: Wmi))) by A13, A14;

 then ( len (( Cage (C,n)) -: Wmi)) >= 2 by NAT_1: 39;

 then

 A23: ( rng (( Cage (C,n)) -: Wmi)) c= ( L~ (( Cage (C,n)) -: Wmi)) by SPPOL_2: 18;



 A24: not Ema in ( rng (( Cage (C,n)) :- Wmi))

 proof

 ((( Cage (C,n)) :- Wmi) /. 1) = Wmi by FINSEQ_5: 53;

 then

 A25: Wmi in ( rng (( Cage (C,n)) :- Wmi)) by FINSEQ_6: 42;

 ((( Cage (C,n)) :- Wmi) /. ( len (( Cage (C,n)) :- Wmi))) = (( Cage (C,n)) /. ( len ( Cage (C,n)))) by A9, FINSEQ_5: 54

 .= (( Cage (C,n)) /. 1) by FINSEQ_6:def 1

 .= Nmi by JORDAN9: 32;

 then

 A26: Nmi in ( rng (( Cage (C,n)) :- Wmi)) by FINSEQ_6: 168;

 {Nmi, Wmi} c= ( rng (( Cage (C,n)) :- Wmi)) by A26, A25, TARSKI:def 2;

 then

 A27: ( card {Nmi, Wmi}) c= ( card ( rng (( Cage (C,n)) :- Wmi))) by CARD_1: 11;



 A28: (Nmi `2 ) = ( N-bound ( L~ ( Cage (C,n)))) by EUCLID: 52;

 Wma in ( L~ ( Cage (C,n))) by SPRECT_1: 13;

 then (Wma `2 ) <= (Nmi `2 ) by A28, PSCOMP_1: 24;

 then Nmi <> Wmi by SPRECT_2: 57;

 then

 A29: ( card {Nmi, Wmi}) = 2 by CARD_2: 57;

 ( card ( rng (( Cage (C,n)) :- Wmi))) c= ( card ( dom (( Cage (C,n)) :- Wmi))) by CARD_2: 61;

 then ( card ( rng (( Cage (C,n)) :- Wmi))) c= ( len (( Cage (C,n)) :- Wmi)) by CARD_1: 62;

 then ( Segm 2) c= ( Segm ( len (( Cage (C,n)) :- Wmi))) by A29, A27;

 then ( len (( Cage (C,n)) :- Wmi)) >= 2 by NAT_1: 39;

 then

 A30: ( rng (( Cage (C,n)) :- Wmi)) c= ( L~ (( Cage (C,n)) :- Wmi)) by SPPOL_2: 18;

 assume Ema in ( rng (( Cage (C,n)) :- Wmi));

 then Ema in (( L~ (( Cage (C,n)) -: Wmi)) /\ ( L~ (( Cage (C,n)) :- Wmi))) by A20, A23, A30, XBOOLE_0:def 4;

 then Ema in {Nmi, Wmi} by JORDAN1G: 17;

 then Ema = Wmi by A17, TARSKI:def 2;

 hence contradiction by TOPREAL5: 19;

 end;



 A31: (Nma .. ( Cage (C,n))) <= (Ema .. ( Cage (C,n))) by A2, SPRECT_2: 70;



 A32: (Nmi .. ( Cage (C,n))) < (Nma .. ( Cage (C,n))) by A2, SPRECT_2: 68;

 then

 A33: (Nmi .. ( Cage (C,n))) < (Ema .. ( Cage (C,n))) by A2, SPRECT_2: 70, XXREAL_0: 2;

 then

 A34: Nmi in ( rng (( Cage (C,n)) -: Wmi)) by A1, A9, A4, FINSEQ_5: 46, XXREAL_0: 2;



 A35: (Ema .. (( Cage (C,n)) -: Wmi)) <> 1

 proof

 assume

 A36: (Ema .. (( Cage (C,n)) -: Wmi)) = 1;

 (Nmi .. (( Cage (C,n)) -: Wmi)) = (Nmi .. ( Cage (C,n))) by A1, A9, A33, A4, SPRECT_5: 3, XXREAL_0: 2

 .= 1 by A2, FINSEQ_6: 43;

 hence contradiction by A32, A31, A20, A34, A36, FINSEQ_5: 9;

 end;

 then Ema in ( rng ((( Cage (C,n)) -: Wmi) /^ 1)) by A20, FINSEQ_6: 78;

 then

 A37: Ema in (( rng ((( Cage (C,n)) -: Wmi) /^ 1)) \ ( rng (( Cage (C,n)) :- Wmi))) by A24, XBOOLE_0:def 5;

 ( card ( rng (( Cage (C,n)) :- Ema))) c= ( card ( dom (( Cage (C,n)) :- Ema))) by CARD_2: 61;

 then ( card ( rng (( Cage (C,n)) :- Ema))) c= ( len (( Cage (C,n)) :- Ema)) by CARD_1: 62;

 then ( Segm 2) c= ( Segm ( len (( Cage (C,n)) :- Ema))) by A18, A8;

 then ( len (( Cage (C,n)) :- Ema)) >= 2 by NAT_1: 39;

 then

 A38: ( rng (( Cage (C,n)) :- Ema)) c= ( L~ (( Cage (C,n)) :- Ema)) by SPPOL_2: 18;

 not Wmi in ( rng (( Cage (C,n)) -: Ema))

 proof

 assume

 A39: Wmi in ( rng (( Cage (C,n)) -: Ema));

 ((( Cage (C,n)) -: Ema) /. ( len (( Cage (C,n)) -: Ema))) = ((( Cage (C,n)) -: Ema) /. (Ema .. ( Cage (C,n)))) by A6, FINSEQ_5: 42

 .= Ema by A6, FINSEQ_5: 45;

 then

 A40: Ema in ( rng (( Cage (C,n)) -: Ema)) by A39, RELAT_1: 38, FINSEQ_6: 168;

 ((( Cage (C,n)) -: Ema) /. 1) = (( Cage (C,n)) /. 1) by A6, FINSEQ_5: 44

 .= Nmi by JORDAN9: 32;

 then

 A41: Nmi in ( rng (( Cage (C,n)) -: Ema)) by A39, FINSEQ_6: 42, RELAT_1: 38;

 {Nmi, Ema} c= ( rng (( Cage (C,n)) -: Ema)) by A41, A40, TARSKI:def 2;

 then

 A42: ( card {Nmi, Ema}) c= ( card ( rng (( Cage (C,n)) -: Ema))) by CARD_1: 11;

 ( card ( rng (( Cage (C,n)) -: Ema))) c= ( card ( dom (( Cage (C,n)) -: Ema))) by CARD_2: 61;

 then ( card ( rng (( Cage (C,n)) -: Ema))) c= ( len (( Cage (C,n)) -: Ema)) by CARD_1: 62;

 then ( Segm 2) c= ( Segm ( len (( Cage (C,n)) -: Ema))) by A18, A42;

 then ( len (( Cage (C,n)) -: Ema)) >= 2 by NAT_1: 39;

 then ( rng (( Cage (C,n)) -: Ema)) c= ( L~ (( Cage (C,n)) -: Ema)) by SPPOL_2: 18;

 then Wmi in (( L~ (( Cage (C,n)) -: Ema)) /\ ( L~ (( Cage (C,n)) :- Ema))) by A21, A38, A39, XBOOLE_0:def 4;

 then Wmi in {Nmi, Ema} by Th3;

 then Wmi = Ema by A22, TARSKI:def 2;

 hence contradiction by TOPREAL5: 19;

 end;

 then

 A43: Wmi in (( rng ( Cage (C,n))) \ ( rng (( Cage (C,n)) -: Ema))) by A9, XBOOLE_0:def 5;

 (RotWmi -: Ema) = (((( Cage (C,n)) :- Wmi) ^ ((( Cage (C,n)) -: Wmi) /^ 1)) -: Ema) by A9, FINSEQ_6:def 2

 .= ((( Cage (C,n)) :- Wmi) ^ (((( Cage (C,n)) -: Wmi) /^ 1) -: Ema)) by A37, FINSEQ_6: 67

 .= ((( Cage (C,n)) :- Wmi) ^ (((( Cage (C,n)) -: Wmi) -: Ema) /^ 1)) by A20, A35, FINSEQ_6: 60

 .= (((( Cage (C,n)) :- Ema) :- Wmi) ^ (((( Cage (C,n)) -: Wmi) -: Ema) /^ 1)) by A43, FINSEQ_6: 71, SPRECT_2: 46

 .= (((( Cage (C,n)) :- Ema) :- Wmi) ^ ((( Cage (C,n)) -: Ema) /^ 1)) by A9, A20, FINSEQ_6: 75

 .= (((( Cage (C,n)) :- Ema) ^ ((( Cage (C,n)) -: Ema) /^ 1)) :- Wmi) by A21, FINSEQ_6: 64

 .= (RotEma :- Wmi) by A6, FINSEQ_6:def 2;

 hence thesis by JORDAN1E:def 1;

 end;

 theorem :: JORDAN1J:5

 for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds ( W-min ( L~ ( Cage (C,n)))) in ( rng ( Upper_Seq (C,n))) & ( W-min ( L~ ( Cage (C,n)))) in ( L~ ( Upper_Seq (C,n)))

 proof

 let C be compact non vertical non horizontal Subset of ( TOP-REAL 2);

 set p = ( W-min ( L~ ( Cage (C,n))));



 A1: p in ( rng ( Cage (C,n))) by SPRECT_2: 43;

 ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 46;

 then

 A2: ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Rotate (( Cage (C,n)),p))) by FINSEQ_6: 90, SPRECT_2: 43;

 ( Upper_Seq (C,n)) = (( Rotate (( Cage (C,n)),p)) -: ( E-max ( L~ ( Cage (C,n))))) by JORDAN1E:def 1;

 then (( Upper_Seq (C,n)) /. 1) = (( Rotate (( Cage (C,n)),p)) /. 1) by A2, FINSEQ_5: 44;

 then (( Upper_Seq (C,n)) /. 1) = p by A1, FINSEQ_6: 92;

 hence

 A3: p in ( rng ( Upper_Seq (C,n))) by FINSEQ_6: 42;

 ( len ( Upper_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 then ( rng ( Upper_Seq (C,n))) c= ( L~ ( Upper_Seq (C,n))) by SPPOL_2: 18;

 hence thesis by A3;

 end;

 theorem :: JORDAN1J:6

 for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds ( W-max ( L~ ( Cage (C,n)))) in ( rng ( Upper_Seq (C,n))) & ( W-max ( L~ ( Cage (C,n)))) in ( L~ ( Upper_Seq (C,n)))

 proof

 let C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2);

 set x = ( W-max ( L~ ( Cage (C,n))));

 set p = ( W-min ( L~ ( Cage (C,n))));

 set f = ( Rotate (( Cage (C,n)),( E-max ( L~ ( Cage (C,n))))));



 A1: ( rng f) = ( rng ( Cage (C,n))) by FINSEQ_6: 90, SPRECT_2: 46;



 A2: x in ( rng ( Cage (C,n))) by SPRECT_2: 44;



 A3: ( L~ ( Cage (C,n))) = ( L~ f) by REVROT_1: 33;

 ( W-min ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 43;

 then

 A4: ( W-min ( L~ ( Cage (C,n)))) in ( rng f) by FINSEQ_6: 90, SPRECT_2: 46;



 A5: p in ( rng ( Cage (C,n))) by SPRECT_2: 43;

 ( Lower_Seq (C,n)) = (f -: ( W-min ( L~ ( Cage (C,n))))) by JORDAN1G: 18;

 then (( Lower_Seq (C,n)) /. 1) = (f /. 1) by A4, FINSEQ_5: 44;

 then (( W-min ( L~ f)) .. f) < (( W-max ( L~ f)) .. f) by A3, JORDAN1F: 6, SPRECT_5: 42;

 then x in ( rng (f :- p)) by A1, A2, A5, A3, FINSEQ_6: 62;

 hence

 A6: x in ( rng ( Upper_Seq (C,n))) by Th4;

 ( len ( Upper_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 then ( rng ( Upper_Seq (C,n))) c= ( L~ ( Upper_Seq (C,n))) by SPPOL_2: 18;

 hence thesis by A6;

 end;

 theorem :: JORDAN1J:7



 Th7: for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds ( N-min ( L~ ( Cage (C,n)))) in ( rng ( Upper_Seq (C,n))) & ( N-min ( L~ ( Cage (C,n)))) in ( L~ ( Upper_Seq (C,n)))

 proof

 let C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2);

 set x = ( N-min ( L~ ( Cage (C,n))));

 set p = ( W-min ( L~ ( Cage (C,n))));

 set f = ( Rotate (( Cage (C,n)),( E-max ( L~ ( Cage (C,n))))));



 A1: ( rng f) = ( rng ( Cage (C,n))) by FINSEQ_6: 90, SPRECT_2: 46;



 A2: x in ( rng ( Cage (C,n))) by SPRECT_2: 39;



 A3: ( L~ ( Cage (C,n))) = ( L~ f) by REVROT_1: 33;

 ( W-min ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 43;

 then

 A4: ( W-min ( L~ ( Cage (C,n)))) in ( rng f) by FINSEQ_6: 90, SPRECT_2: 46;



 A5: p in ( rng ( Cage (C,n))) by SPRECT_2: 43;

 ( Lower_Seq (C,n)) = (f -: ( W-min ( L~ ( Cage (C,n))))) by JORDAN1G: 18;

 then

 A6: (( Lower_Seq (C,n)) /. 1) = (f /. 1) by A4, FINSEQ_5: 44;

 then

 A7: (( W-max ( L~ f)) .. f) <= (( N-min ( L~ f)) .. f) by A3, JORDAN1F: 6, SPRECT_5: 43;

 (( W-min ( L~ f)) .. f) < (( W-max ( L~ f)) .. f) by A6, A3, JORDAN1F: 6, SPRECT_5: 42;

 then x in ( rng (f :- p)) by A1, A2, A5, A3, A7, FINSEQ_6: 62, XXREAL_0: 2;

 hence

 A8: x in ( rng ( Upper_Seq (C,n))) by Th4;

 ( len ( Upper_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 then ( rng ( Upper_Seq (C,n))) c= ( L~ ( Upper_Seq (C,n))) by SPPOL_2: 18;

 hence thesis by A8;

 end;

 theorem :: JORDAN1J:8

 for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds ( N-max ( L~ ( Cage (C,n)))) in ( rng ( Upper_Seq (C,n))) & ( N-max ( L~ ( Cage (C,n)))) in ( L~ ( Upper_Seq (C,n)))

 proof

 let C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2);

 set x = ( N-max ( L~ ( Cage (C,n))));

 set p = ( W-min ( L~ ( Cage (C,n))));

 set f = ( Rotate (( Cage (C,n)),( E-max ( L~ ( Cage (C,n))))));



 A1: ( rng f) = ( rng ( Cage (C,n))) by FINSEQ_6: 90, SPRECT_2: 46;



 A2: x in ( rng ( Cage (C,n))) by SPRECT_2: 40;



 A3: (( Lower_Seq (C,n)) /. 1) = ( E-max ( L~ ( Cage (C,n)))) by JORDAN1F: 6;



 A4: ( L~ ( Cage (C,n))) = ( L~ f) by REVROT_1: 33;

 ( W-min ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 43;

 then

 A5: ( W-min ( L~ ( Cage (C,n)))) in ( rng f) by FINSEQ_6: 90, SPRECT_2: 46;



 A6: p in ( rng ( Cage (C,n))) by SPRECT_2: 43;

 ( Lower_Seq (C,n)) = (f -: ( W-min ( L~ ( Cage (C,n))))) by JORDAN1G: 18;

 then

 A7: (( Lower_Seq (C,n)) /. 1) = (f /. 1) by A5, FINSEQ_5: 44;

 then

 A8: (( W-min ( L~ f)) .. f) < (( W-max ( L~ f)) .. f) by A4, JORDAN1F: 6, SPRECT_5: 42;



 A9: (( W-max ( L~ f)) .. f) <= (( N-min ( L~ f)) .. f) by A7, A4, JORDAN1F: 6, SPRECT_5: 43;

 per cases ;

 suppose ( N-max ( L~ f)) <> ( E-max ( L~ f));

 then (( W-max ( L~ f)) .. f) < (( N-max ( L~ f)) .. f) by A7, A3, A4, A9, SPRECT_5: 44, XXREAL_0: 2;

 then x in ( rng (f :- p)) by A1, A2, A6, A4, A8, FINSEQ_6: 62, XXREAL_0: 2;

 hence

 A10: x in ( rng ( Upper_Seq (C,n))) by Th4;

 ( len ( Upper_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 then ( rng ( Upper_Seq (C,n))) c= ( L~ ( Upper_Seq (C,n))) by SPPOL_2: 18;

 hence thesis by A10;

 end;

 suppose

 A11: ( N-max ( L~ f)) = ( E-max ( L~ f));



 A12: (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) <= (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))));

 ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 46;

 then

 A13: ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by FINSEQ_6: 90, SPRECT_2: 43;

 ( Upper_Seq (C,n)) = (( Rotate (( Cage (C,n)),p)) -: ( E-max ( L~ ( Cage (C,n))))) by JORDAN1E:def 1;

 hence

 A14: x in ( rng ( Upper_Seq (C,n))) by A4, A11, A13, A12, FINSEQ_5: 46;

 ( len ( Upper_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 then ( rng ( Upper_Seq (C,n))) c= ( L~ ( Upper_Seq (C,n))) by SPPOL_2: 18;

 hence thesis by A14;

 end;

 end;

 theorem :: JORDAN1J:9

 for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Upper_Seq (C,n))) & ( E-max ( L~ ( Cage (C,n)))) in ( L~ ( Upper_Seq (C,n)))

 proof

 let C be compact non vertical non horizontal Subset of ( TOP-REAL 2);

 set x = ( E-max ( L~ ( Cage (C,n))));

 set p = ( W-min ( L~ ( Cage (C,n))));



 A1: (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) <= (( E-max ( L~ ( Cage (C,n)))) .. ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))));

 ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 46;

 then

 A2: ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))))) by FINSEQ_6: 90, SPRECT_2: 43;

 ( Upper_Seq (C,n)) = (( Rotate (( Cage (C,n)),p)) -: ( E-max ( L~ ( Cage (C,n))))) by JORDAN1E:def 1;

 hence

 A3: x in ( rng ( Upper_Seq (C,n))) by A2, A1, FINSEQ_5: 46;

 ( len ( Upper_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 then ( rng ( Upper_Seq (C,n))) c= ( L~ ( Upper_Seq (C,n))) by SPPOL_2: 18;

 hence thesis by A3;

 end;

 theorem :: JORDAN1J:10

 for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Lower_Seq (C,n))) & ( E-max ( L~ ( Cage (C,n)))) in ( L~ ( Lower_Seq (C,n)))

 proof

 let C be compact non vertical non horizontal Subset of ( TOP-REAL 2);

 set p = ( E-max ( L~ ( Cage (C,n))));

 ( Lower_Seq (C,n)) = (( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n)))))) :- p) by JORDAN1E:def 2;

 hence

 A1: p in ( rng ( Lower_Seq (C,n))) by FINSEQ_6: 61;

 ( len ( Lower_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 then ( rng ( Lower_Seq (C,n))) c= ( L~ ( Lower_Seq (C,n))) by SPPOL_2: 18;

 hence thesis by A1;

 end;

 theorem :: JORDAN1J:11

 for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds ( E-min ( L~ ( Cage (C,n)))) in ( rng ( Lower_Seq (C,n))) & ( E-min ( L~ ( Cage (C,n)))) in ( L~ ( Lower_Seq (C,n)))

 proof

 let C be compact non vertical non horizontal Subset of ( TOP-REAL 2);

 set x = ( E-min ( L~ ( Cage (C,n))));

 set p = ( E-max ( L~ ( Cage (C,n))));

 set f = ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))));



 A1: ( rng f) = ( rng ( Cage (C,n))) by FINSEQ_6: 90, SPRECT_2: 43;



 A2: x in ( rng ( Cage (C,n))) by SPRECT_2: 45;



 A3: ( L~ ( Cage (C,n))) = ( L~ f) by REVROT_1: 33;

 ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 46;

 then

 A4: ( E-max ( L~ ( Cage (C,n)))) in ( rng f) by FINSEQ_6: 90, SPRECT_2: 43;



 A5: p in ( rng ( Cage (C,n))) by SPRECT_2: 46;

 ( Upper_Seq (C,n)) = (f -: ( E-max ( L~ ( Cage (C,n))))) by JORDAN1E:def 1;

 then (( Upper_Seq (C,n)) /. 1) = (f /. 1) by A4, FINSEQ_5: 44;

 then (( E-max ( L~ f)) .. f) < (( E-min ( L~ f)) .. f) by A3, JORDAN1F: 5, SPRECT_5: 26;

 then x in ( rng (f :- p)) by A1, A2, A5, A3, FINSEQ_6: 62;

 hence

 A6: x in ( rng ( Lower_Seq (C,n))) by JORDAN1E:def 2;

 ( len ( Lower_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 then ( rng ( Lower_Seq (C,n))) c= ( L~ ( Lower_Seq (C,n))) by SPPOL_2: 18;

 hence thesis by A6;

 end;

 theorem :: JORDAN1J:12



 Th12: for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds ( S-max ( L~ ( Cage (C,n)))) in ( rng ( Lower_Seq (C,n))) & ( S-max ( L~ ( Cage (C,n)))) in ( L~ ( Lower_Seq (C,n)))

 proof

 let C be compact non vertical non horizontal Subset of ( TOP-REAL 2);

 set x = ( S-max ( L~ ( Cage (C,n))));

 set p = ( E-max ( L~ ( Cage (C,n))));

 set f = ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))));



 A1: ( rng f) = ( rng ( Cage (C,n))) by FINSEQ_6: 90, SPRECT_2: 43;



 A2: x in ( rng ( Cage (C,n))) by SPRECT_2: 42;



 A3: ( L~ ( Cage (C,n))) = ( L~ f) by REVROT_1: 33;

 ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 46;

 then

 A4: ( E-max ( L~ ( Cage (C,n)))) in ( rng f) by FINSEQ_6: 90, SPRECT_2: 43;



 A5: p in ( rng ( Cage (C,n))) by SPRECT_2: 46;

 ( Upper_Seq (C,n)) = (f -: ( E-max ( L~ ( Cage (C,n))))) by JORDAN1E:def 1;

 then

 A6: (( Upper_Seq (C,n)) /. 1) = (f /. 1) by A4, FINSEQ_5: 44;

 then

 A7: (( E-min ( L~ f)) .. f) <= (( S-max ( L~ f)) .. f) by A3, JORDAN1F: 5, SPRECT_5: 27;

 (( E-max ( L~ f)) .. f) < (( E-min ( L~ f)) .. f) by A6, A3, JORDAN1F: 5, SPRECT_5: 26;

 then x in ( rng (f :- p)) by A1, A2, A5, A3, A7, FINSEQ_6: 62, XXREAL_0: 2;

 hence

 A8: x in ( rng ( Lower_Seq (C,n))) by JORDAN1E:def 2;

 ( len ( Lower_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 then ( rng ( Lower_Seq (C,n))) c= ( L~ ( Lower_Seq (C,n))) by SPPOL_2: 18;

 hence thesis by A8;

 end;

 theorem :: JORDAN1J:13

 for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds ( S-min ( L~ ( Cage (C,n)))) in ( rng ( Lower_Seq (C,n))) & ( S-min ( L~ ( Cage (C,n)))) in ( L~ ( Lower_Seq (C,n)))

 proof

 let C be compact non vertical non horizontal Subset of ( TOP-REAL 2);

 set x = ( S-min ( L~ ( Cage (C,n))));

 set p = ( E-max ( L~ ( Cage (C,n))));

 set f = ( Rotate (( Cage (C,n)),( W-min ( L~ ( Cage (C,n))))));



 A1: ( rng f) = ( rng ( Cage (C,n))) by FINSEQ_6: 90, SPRECT_2: 43;



 A2: x in ( rng ( Cage (C,n))) by SPRECT_2: 41;



 A3: (( Upper_Seq (C,n)) /. 1) = ( W-min ( L~ ( Cage (C,n)))) by JORDAN1F: 5;



 A4: ( L~ ( Cage (C,n))) = ( L~ f) by REVROT_1: 33;

 ( E-max ( L~ ( Cage (C,n)))) in ( rng ( Cage (C,n))) by SPRECT_2: 46;

 then

 A5: ( E-max ( L~ ( Cage (C,n)))) in ( rng f) by FINSEQ_6: 90, SPRECT_2: 43;



 A6: p in ( rng ( Cage (C,n))) by SPRECT_2: 46;

 ( Upper_Seq (C,n)) = (f -: ( E-max ( L~ ( Cage (C,n))))) by JORDAN1E:def 1;

 then

 A7: (( Upper_Seq (C,n)) /. 1) = (f /. 1) by A5, FINSEQ_5: 44;

 then

 A8: (( E-max ( L~ f)) .. f) < (( E-min ( L~ f)) .. f) by A4, JORDAN1F: 5, SPRECT_5: 26;



 A9: (( E-min ( L~ f)) .. f) <= (( S-max ( L~ f)) .. f) by A7, A4, JORDAN1F: 5, SPRECT_5: 27;

 per cases ;

 suppose ( S-min ( L~ f)) <> ( W-min ( L~ f));

 then (( E-min ( L~ f)) .. f) < (( S-min ( L~ f)) .. f) by A7, A3, A4, A9, SPRECT_5: 28, XXREAL_0: 2;

 then x in ( rng (f :- p)) by A1, A2, A6, A4, A8, FINSEQ_6: 62, XXREAL_0: 2;

 hence

 A10: x in ( rng ( Lower_Seq (C,n))) by JORDAN1E:def 2;

 ( len ( Lower_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 then ( rng ( Lower_Seq (C,n))) c= ( L~ ( Lower_Seq (C,n))) by SPPOL_2: 18;

 hence thesis by A10;

 end;

 suppose

 A11: ( S-min ( L~ f)) = ( W-min ( L~ f));

 (( Lower_Seq (C,n)) /. ( len ( Lower_Seq (C,n)))) = ( W-min ( L~ ( Cage (C,n)))) by JORDAN1F: 8;

 hence

 A12: x in ( rng ( Lower_Seq (C,n))) by A4, A11, FINSEQ_6: 168;

 ( len ( Lower_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 then ( rng ( Lower_Seq (C,n))) c= ( L~ ( Lower_Seq (C,n))) by SPPOL_2: 18;

 hence thesis by A12;

 end;

 end;

 theorem :: JORDAN1J:14

 for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds ( W-min ( L~ ( Cage (C,n)))) in ( rng ( Lower_Seq (C,n))) & ( W-min ( L~ ( Cage (C,n)))) in ( L~ ( Lower_Seq (C,n)))

 proof

 let C be compact non vertical non horizontal Subset of ( TOP-REAL 2);

 set p = ( W-min ( L~ ( Cage (C,n))));

 (( Lower_Seq (C,n)) /. ( len ( Lower_Seq (C,n)))) = p by JORDAN1F: 8;

 hence

 A1: p in ( rng ( Lower_Seq (C,n))) by FINSEQ_6: 168;

 ( len ( Lower_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 then ( rng ( Lower_Seq (C,n))) c= ( L~ ( Lower_Seq (C,n))) by SPPOL_2: 18;

 hence thesis by A1;

 end;

 theorem :: JORDAN1J:15



 Th15: for X,Y be non empty compact Subset of ( TOP-REAL 2) st X c= Y & ( N-min Y) in X holds ( N-min X) = ( N-min Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume that

 A1: X c= Y and

 A2: ( N-min Y) in X;



 A3: ( N-bound X) >= (( N-min Y) `2 ) by A2, PSCOMP_1: 24;



 A4: (( N-min X) `2 ) = ( N-bound X) by EUCLID: 52;



 A5: (( N-min Y) `2 ) = ( N-bound Y) by EUCLID: 52;



 A6: ( N-bound X) <= ( N-bound Y) by A1, PSCOMP_1: 66;

 then

 A7: ( N-bound X) = ( N-bound Y) by A5, A3, XXREAL_0: 1;

 ( N-min Y) in ( N-most X) by A2, A6, A5, A3, SPRECT_2: 10, XXREAL_0: 1;

 then

 A8: (( N-min X) `1 ) <= (( N-min Y) `1 ) by PSCOMP_1: 39;

 ( N-min X) in X by SPRECT_1: 11;

 then ( N-min X) in ( N-most Y) by A1, A6, A4, A5, A3, SPRECT_2: 10, XXREAL_0: 1;

 then (( N-min X) `1 ) >= (( N-min Y) `1 ) by PSCOMP_1: 39;

 then (( N-min X) `1 ) = (( N-min Y) `1 ) by A8, XXREAL_0: 1;

 hence thesis by A4, A5, A7, TOPREAL3: 6;

 end;

 theorem :: JORDAN1J:16



 Th16: for X,Y be non empty compact Subset of ( TOP-REAL 2) st X c= Y & ( N-max Y) in X holds ( N-max X) = ( N-max Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume that

 A1: X c= Y and

 A2: ( N-max Y) in X;



 A3: ( N-bound X) >= (( N-max Y) `2 ) by A2, PSCOMP_1: 24;



 A4: (( N-max X) `2 ) = ( N-bound X) by EUCLID: 52;



 A5: (( N-max Y) `2 ) = ( N-bound Y) by EUCLID: 52;



 A6: ( N-bound X) <= ( N-bound Y) by A1, PSCOMP_1: 66;

 then

 A7: ( N-bound X) = ( N-bound Y) by A5, A3, XXREAL_0: 1;

 ( N-max Y) in ( N-most X) by A2, A6, A5, A3, SPRECT_2: 10, XXREAL_0: 1;

 then

 A8: (( N-max X) `1 ) >= (( N-max Y) `1 ) by PSCOMP_1: 39;

 ( N-max X) in X by SPRECT_1: 11;

 then ( N-max X) in ( N-most Y) by A1, A6, A4, A5, A3, SPRECT_2: 10, XXREAL_0: 1;

 then (( N-max X) `1 ) <= (( N-max Y) `1 ) by PSCOMP_1: 39;

 then (( N-max X) `1 ) = (( N-max Y) `1 ) by A8, XXREAL_0: 1;

 hence thesis by A4, A5, A7, TOPREAL3: 6;

 end;

 theorem :: JORDAN1J:17



 Th17: for X,Y be non empty compact Subset of ( TOP-REAL 2) st X c= Y & ( E-min Y) in X holds ( E-min X) = ( E-min Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume that

 A1: X c= Y and

 A2: ( E-min Y) in X;



 A3: ( E-bound X) >= (( E-min Y) `1 ) by A2, PSCOMP_1: 24;



 A4: (( E-min X) `1 ) = ( E-bound X) by EUCLID: 52;



 A5: (( E-min Y) `1 ) = ( E-bound Y) by EUCLID: 52;



 A6: ( E-bound X) <= ( E-bound Y) by A1, PSCOMP_1: 67;

 then

 A7: ( E-bound X) = ( E-bound Y) by A5, A3, XXREAL_0: 1;

 ( E-min Y) in ( E-most X) by A2, A6, A5, A3, SPRECT_2: 13, XXREAL_0: 1;

 then

 A8: (( E-min X) `2 ) <= (( E-min Y) `2 ) by PSCOMP_1: 47;

 ( E-min X) in X by SPRECT_1: 14;

 then ( E-min X) in ( E-most Y) by A1, A6, A4, A5, A3, SPRECT_2: 13, XXREAL_0: 1;

 then (( E-min X) `2 ) >= (( E-min Y) `2 ) by PSCOMP_1: 47;

 then (( E-min X) `2 ) = (( E-min Y) `2 ) by A8, XXREAL_0: 1;

 hence thesis by A4, A5, A7, TOPREAL3: 6;

 end;

 theorem :: JORDAN1J:18



 Th18: for X,Y be non empty compact Subset of ( TOP-REAL 2) st X c= Y & ( E-max Y) in X holds ( E-max X) = ( E-max Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume that

 A1: X c= Y and

 A2: ( E-max Y) in X;



 A3: ( E-bound X) >= (( E-max Y) `1 ) by A2, PSCOMP_1: 24;



 A4: (( E-max X) `1 ) = ( E-bound X) by EUCLID: 52;



 A5: (( E-max Y) `1 ) = ( E-bound Y) by EUCLID: 52;



 A6: ( E-bound X) <= ( E-bound Y) by A1, PSCOMP_1: 67;

 then

 A7: ( E-bound X) = ( E-bound Y) by A5, A3, XXREAL_0: 1;

 ( E-max Y) in ( E-most X) by A2, A6, A5, A3, SPRECT_2: 13, XXREAL_0: 1;

 then

 A8: (( E-max X) `2 ) >= (( E-max Y) `2 ) by PSCOMP_1: 47;

 ( E-max X) in X by SPRECT_1: 14;

 then ( E-max X) in ( E-most Y) by A1, A6, A4, A5, A3, SPRECT_2: 13, XXREAL_0: 1;

 then (( E-max X) `2 ) <= (( E-max Y) `2 ) by PSCOMP_1: 47;

 then (( E-max X) `2 ) = (( E-max Y) `2 ) by A8, XXREAL_0: 1;

 hence thesis by A4, A5, A7, TOPREAL3: 6;

 end;

 theorem :: JORDAN1J:19



 Th19: for X,Y be non empty compact Subset of ( TOP-REAL 2) st X c= Y & ( S-min Y) in X holds ( S-min X) = ( S-min Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume that

 A1: X c= Y and

 A2: ( S-min Y) in X;



 A3: ( S-bound X) <= (( S-min Y) `2 ) by A2, PSCOMP_1: 24;



 A4: (( S-min X) `2 ) = ( S-bound X) by EUCLID: 52;



 A5: (( S-min Y) `2 ) = ( S-bound Y) by EUCLID: 52;



 A6: ( S-bound X) >= ( S-bound Y) by A1, PSCOMP_1: 68;

 then

 A7: ( S-bound X) = ( S-bound Y) by A5, A3, XXREAL_0: 1;

 ( S-min Y) in ( S-most X) by A2, A6, A5, A3, SPRECT_2: 11, XXREAL_0: 1;

 then

 A8: (( S-min X) `1 ) <= (( S-min Y) `1 ) by PSCOMP_1: 55;

 ( S-min X) in X by SPRECT_1: 12;

 then ( S-min X) in ( S-most Y) by A1, A6, A4, A5, A3, SPRECT_2: 11, XXREAL_0: 1;

 then (( S-min X) `1 ) >= (( S-min Y) `1 ) by PSCOMP_1: 55;

 then (( S-min X) `1 ) = (( S-min Y) `1 ) by A8, XXREAL_0: 1;

 hence thesis by A4, A5, A7, TOPREAL3: 6;

 end;

 theorem :: JORDAN1J:20



 Th20: for X,Y be non empty compact Subset of ( TOP-REAL 2) st X c= Y & ( S-max Y) in X holds ( S-max X) = ( S-max Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume that

 A1: X c= Y and

 A2: ( S-max Y) in X;



 A3: ( S-bound X) <= (( S-max Y) `2 ) by A2, PSCOMP_1: 24;



 A4: (( S-max X) `2 ) = ( S-bound X) by EUCLID: 52;



 A5: (( S-max Y) `2 ) = ( S-bound Y) by EUCLID: 52;



 A6: ( S-bound X) >= ( S-bound Y) by A1, PSCOMP_1: 68;

 then

 A7: ( S-bound X) = ( S-bound Y) by A5, A3, XXREAL_0: 1;

 ( S-max Y) in ( S-most X) by A2, A6, A5, A3, SPRECT_2: 11, XXREAL_0: 1;

 then

 A8: (( S-max X) `1 ) >= (( S-max Y) `1 ) by PSCOMP_1: 55;

 ( S-max X) in X by SPRECT_1: 12;

 then ( S-max X) in ( S-most Y) by A1, A6, A4, A5, A3, SPRECT_2: 11, XXREAL_0: 1;

 then (( S-max X) `1 ) <= (( S-max Y) `1 ) by PSCOMP_1: 55;

 then (( S-max X) `1 ) = (( S-max Y) `1 ) by A8, XXREAL_0: 1;

 hence thesis by A4, A5, A7, TOPREAL3: 6;

 end;

 theorem :: JORDAN1J:21



 Th21: for X,Y be non empty compact Subset of ( TOP-REAL 2) st X c= Y & ( W-min Y) in X holds ( W-min X) = ( W-min Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume that

 A1: X c= Y and

 A2: ( W-min Y) in X;



 A3: ( W-bound X) <= (( W-min Y) `1 ) by A2, PSCOMP_1: 24;



 A4: (( W-min X) `1 ) = ( W-bound X) by EUCLID: 52;



 A5: (( W-min Y) `1 ) = ( W-bound Y) by EUCLID: 52;



 A6: ( W-bound X) >= ( W-bound Y) by A1, PSCOMP_1: 69;

 then

 A7: ( W-bound X) = ( W-bound Y) by A5, A3, XXREAL_0: 1;

 ( W-min Y) in ( W-most X) by A2, A6, A5, A3, SPRECT_2: 12, XXREAL_0: 1;

 then

 A8: (( W-min X) `2 ) <= (( W-min Y) `2 ) by PSCOMP_1: 31;

 ( W-min X) in X by SPRECT_1: 13;

 then ( W-min X) in ( W-most Y) by A1, A6, A4, A5, A3, SPRECT_2: 12, XXREAL_0: 1;

 then (( W-min X) `2 ) >= (( W-min Y) `2 ) by PSCOMP_1: 31;

 then (( W-min X) `2 ) = (( W-min Y) `2 ) by A8, XXREAL_0: 1;

 hence thesis by A4, A5, A7, TOPREAL3: 6;

 end;

 theorem :: JORDAN1J:22



 Th22: for X,Y be non empty compact Subset of ( TOP-REAL 2) st X c= Y & ( W-max Y) in X holds ( W-max X) = ( W-max Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume that

 A1: X c= Y and

 A2: ( W-max Y) in X;



 A3: ( W-bound X) <= (( W-max Y) `1 ) by A2, PSCOMP_1: 24;



 A4: (( W-max X) `1 ) = ( W-bound X) by EUCLID: 52;



 A5: (( W-max Y) `1 ) = ( W-bound Y) by EUCLID: 52;



 A6: ( W-bound X) >= ( W-bound Y) by A1, PSCOMP_1: 69;

 then

 A7: ( W-bound X) = ( W-bound Y) by A5, A3, XXREAL_0: 1;

 ( W-max Y) in ( W-most X) by A2, A6, A5, A3, SPRECT_2: 12, XXREAL_0: 1;

 then

 A8: (( W-max X) `2 ) >= (( W-max Y) `2 ) by PSCOMP_1: 31;

 ( W-max X) in X by SPRECT_1: 13;

 then ( W-max X) in ( W-most Y) by A1, A6, A4, A5, A3, SPRECT_2: 12, XXREAL_0: 1;

 then (( W-max X) `2 ) <= (( W-max Y) `2 ) by PSCOMP_1: 31;

 then (( W-max X) `2 ) = (( W-max Y) `2 ) by A8, XXREAL_0: 1;

 hence thesis by A4, A5, A7, TOPREAL3: 6;

 end;

 theorem :: JORDAN1J:23



 Th23: for X,Y be non empty compact Subset of ( TOP-REAL 2) st ( N-bound X) <= ( N-bound Y) holds ( N-bound (X \/ Y)) = ( N-bound Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume ( N-bound X) <= ( N-bound Y);

 then ( max (( N-bound X),( N-bound Y))) = ( N-bound Y) by XXREAL_0:def 10;

 hence thesis by SPRECT_1: 49;

 end;

 theorem :: JORDAN1J:24



 Th24: for X,Y be non empty compact Subset of ( TOP-REAL 2) st ( E-bound X) <= ( E-bound Y) holds ( E-bound (X \/ Y)) = ( E-bound Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume ( E-bound X) <= ( E-bound Y);

 then ( max (( E-bound X),( E-bound Y))) = ( E-bound Y) by XXREAL_0:def 10;

 hence thesis by SPRECT_1: 50;

 end;

 theorem :: JORDAN1J:25



 Th25: for X,Y be non empty compact Subset of ( TOP-REAL 2) st ( S-bound X) <= ( S-bound Y) holds ( S-bound (X \/ Y)) = ( S-bound X)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume ( S-bound X) <= ( S-bound Y);

 then ( min (( S-bound X),( S-bound Y))) = ( S-bound X) by XXREAL_0:def 9;

 hence thesis by SPRECT_1: 48;

 end;

 theorem :: JORDAN1J:26



 Th26: for X,Y be non empty compact Subset of ( TOP-REAL 2) st ( W-bound X) <= ( W-bound Y) holds ( W-bound (X \/ Y)) = ( W-bound X)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume ( W-bound X) <= ( W-bound Y);

 then ( min (( W-bound X),( W-bound Y))) = ( W-bound X) by XXREAL_0:def 9;

 hence thesis by SPRECT_1: 47;

 end;

 theorem :: JORDAN1J:27

 for X,Y be non empty compact Subset of ( TOP-REAL 2) st ( N-bound X) < ( N-bound Y) holds ( N-min (X \/ Y)) = ( N-min Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);



 A1: (( N-min (X \/ Y)) `2 ) = ( N-bound (X \/ Y)) by EUCLID: 52;



 A2: (X \/ Y) is compact by COMPTS_1: 10;

 then

 A3: ( N-min (X \/ Y)) in (X \/ Y) by SPRECT_1: 11;



 A4: ( N-min Y) in Y by SPRECT_1: 11;



 A5: (( N-min Y) `2 ) = ( N-bound Y) by EUCLID: 52;

 assume

 A6: ( N-bound X) < ( N-bound Y);

 then

 A7: ( N-bound (X \/ Y)) = ( N-bound Y) by Th23;

 Y c= (X \/ Y) by XBOOLE_1: 7;

 then ( N-min Y) in ( N-most (X \/ Y)) by A2, A7, A5, A4, SPRECT_2: 10;

 then

 A8: (( N-min (X \/ Y)) `1 ) <= (( N-min Y) `1 ) by A2, PSCOMP_1: 39;

 per cases by A3, XBOOLE_0:def 3;

 suppose ( N-min (X \/ Y)) in Y;

 then ( N-min (X \/ Y)) in ( N-most Y) by A6, A1, Th23, SPRECT_2: 10;

 then (( N-min (X \/ Y)) `1 ) >= (( N-min Y) `1 ) by PSCOMP_1: 39;

 then (( N-min (X \/ Y)) `1 ) = (( N-min Y) `1 ) by A8, XXREAL_0: 1;

 hence thesis by A6, A1, A5, Th23, TOPREAL3: 6;

 end;

 suppose ( N-min (X \/ Y)) in X;

 hence thesis by A6, A7, A1, PSCOMP_1: 24;

 end;

 end;

 theorem :: JORDAN1J:28

 for X,Y be non empty compact Subset of ( TOP-REAL 2) st ( N-bound X) < ( N-bound Y) holds ( N-max (X \/ Y)) = ( N-max Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);



 A1: (( N-max (X \/ Y)) `2 ) = ( N-bound (X \/ Y)) by EUCLID: 52;



 A2: (X \/ Y) is compact by COMPTS_1: 10;

 then

 A3: ( N-max (X \/ Y)) in (X \/ Y) by SPRECT_1: 11;



 A4: ( N-max Y) in Y by SPRECT_1: 11;



 A5: (( N-max Y) `2 ) = ( N-bound Y) by EUCLID: 52;

 assume

 A6: ( N-bound X) < ( N-bound Y);

 then

 A7: ( N-bound (X \/ Y)) = ( N-bound Y) by Th23;

 Y c= (X \/ Y) by XBOOLE_1: 7;

 then ( N-max Y) in ( N-most (X \/ Y)) by A2, A7, A5, A4, SPRECT_2: 10;

 then

 A8: (( N-max (X \/ Y)) `1 ) >= (( N-max Y) `1 ) by A2, PSCOMP_1: 39;

 per cases by A3, XBOOLE_0:def 3;

 suppose ( N-max (X \/ Y)) in Y;

 then ( N-max (X \/ Y)) in ( N-most Y) by A6, A1, Th23, SPRECT_2: 10;

 then (( N-max (X \/ Y)) `1 ) <= (( N-max Y) `1 ) by PSCOMP_1: 39;

 then (( N-max (X \/ Y)) `1 ) = (( N-max Y) `1 ) by A8, XXREAL_0: 1;

 hence thesis by A6, A1, A5, Th23, TOPREAL3: 6;

 end;

 suppose ( N-max (X \/ Y)) in X;

 hence thesis by A6, A7, A1, PSCOMP_1: 24;

 end;

 end;

 theorem :: JORDAN1J:29

 for X,Y be non empty compact Subset of ( TOP-REAL 2) st ( E-bound X) < ( E-bound Y) holds ( E-min (X \/ Y)) = ( E-min Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);



 A1: (( E-min (X \/ Y)) `1 ) = ( E-bound (X \/ Y)) by EUCLID: 52;



 A2: (X \/ Y) is compact by COMPTS_1: 10;

 then

 A3: ( E-min (X \/ Y)) in (X \/ Y) by SPRECT_1: 14;



 A4: ( E-min Y) in Y by SPRECT_1: 14;



 A5: (( E-min Y) `1 ) = ( E-bound Y) by EUCLID: 52;

 assume

 A6: ( E-bound X) < ( E-bound Y);

 then

 A7: ( E-bound (X \/ Y)) = ( E-bound Y) by Th24;

 Y c= (X \/ Y) by XBOOLE_1: 7;

 then ( E-min Y) in ( E-most (X \/ Y)) by A2, A7, A5, A4, SPRECT_2: 13;

 then

 A8: (( E-min (X \/ Y)) `2 ) <= (( E-min Y) `2 ) by A2, PSCOMP_1: 47;

 per cases by A3, XBOOLE_0:def 3;

 suppose ( E-min (X \/ Y)) in Y;

 then ( E-min (X \/ Y)) in ( E-most Y) by A6, A1, Th24, SPRECT_2: 13;

 then (( E-min (X \/ Y)) `2 ) >= (( E-min Y) `2 ) by PSCOMP_1: 47;

 then (( E-min (X \/ Y)) `2 ) = (( E-min Y) `2 ) by A8, XXREAL_0: 1;

 hence thesis by A6, A1, A5, Th24, TOPREAL3: 6;

 end;

 suppose ( E-min (X \/ Y)) in X;

 hence thesis by A6, A7, A1, PSCOMP_1: 24;

 end;

 end;

 theorem :: JORDAN1J:30

 for X,Y be non empty compact Subset of ( TOP-REAL 2) st ( E-bound X) < ( E-bound Y) holds ( E-max (X \/ Y)) = ( E-max Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);



 A1: (( E-max (X \/ Y)) `1 ) = ( E-bound (X \/ Y)) by EUCLID: 52;



 A2: (X \/ Y) is compact by COMPTS_1: 10;

 then

 A3: ( E-max (X \/ Y)) in (X \/ Y) by SPRECT_1: 14;



 A4: ( E-max Y) in Y by SPRECT_1: 14;



 A5: (( E-max Y) `1 ) = ( E-bound Y) by EUCLID: 52;

 assume

 A6: ( E-bound X) < ( E-bound Y);

 then

 A7: ( E-bound (X \/ Y)) = ( E-bound Y) by Th24;

 Y c= (X \/ Y) by XBOOLE_1: 7;

 then ( E-max Y) in ( E-most (X \/ Y)) by A2, A7, A5, A4, SPRECT_2: 13;

 then

 A8: (( E-max (X \/ Y)) `2 ) >= (( E-max Y) `2 ) by A2, PSCOMP_1: 47;

 per cases by A3, XBOOLE_0:def 3;

 suppose ( E-max (X \/ Y)) in Y;

 then ( E-max (X \/ Y)) in ( E-most Y) by A6, A1, Th24, SPRECT_2: 13;

 then (( E-max (X \/ Y)) `2 ) <= (( E-max Y) `2 ) by PSCOMP_1: 47;

 then (( E-max (X \/ Y)) `2 ) = (( E-max Y) `2 ) by A8, XXREAL_0: 1;

 hence thesis by A6, A1, A5, Th24, TOPREAL3: 6;

 end;

 suppose ( E-max (X \/ Y)) in X;

 hence thesis by A6, A7, A1, PSCOMP_1: 24;

 end;

 end;

 theorem :: JORDAN1J:31

 for X,Y be non empty compact Subset of ( TOP-REAL 2) st ( S-bound X) < ( S-bound Y) holds ( S-min (X \/ Y)) = ( S-min X)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);



 A1: (( S-min (X \/ Y)) `2 ) = ( S-bound (X \/ Y)) by EUCLID: 52;



 A2: (X \/ Y) is compact by COMPTS_1: 10;

 then

 A3: ( S-min (X \/ Y)) in (X \/ Y) by SPRECT_1: 12;



 A4: ( S-min X) in X by SPRECT_1: 12;



 A5: (( S-min X) `2 ) = ( S-bound X) by EUCLID: 52;

 assume

 A6: ( S-bound X) < ( S-bound Y);

 then

 A7: ( S-bound (X \/ Y)) = ( S-bound X) by Th25;

 X c= (X \/ Y) by XBOOLE_1: 7;

 then ( S-min X) in ( S-most (X \/ Y)) by A2, A7, A5, A4, SPRECT_2: 11;

 then

 A8: (( S-min (X \/ Y)) `1 ) <= (( S-min X) `1 ) by A2, PSCOMP_1: 55;

 per cases by A3, XBOOLE_0:def 3;

 suppose ( S-min (X \/ Y)) in X;

 then ( S-min (X \/ Y)) in ( S-most X) by A6, A1, Th25, SPRECT_2: 11;

 then (( S-min (X \/ Y)) `1 ) >= (( S-min X) `1 ) by PSCOMP_1: 55;

 then (( S-min (X \/ Y)) `1 ) = (( S-min X) `1 ) by A8, XXREAL_0: 1;

 hence thesis by A6, A1, A5, Th25, TOPREAL3: 6;

 end;

 suppose ( S-min (X \/ Y)) in Y;

 hence thesis by A6, A7, A1, PSCOMP_1: 24;

 end;

 end;

 theorem :: JORDAN1J:32

 for X,Y be non empty compact Subset of ( TOP-REAL 2) st ( S-bound X) < ( S-bound Y) holds ( S-max (X \/ Y)) = ( S-max X)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);



 A1: (( S-max (X \/ Y)) `2 ) = ( S-bound (X \/ Y)) by EUCLID: 52;



 A2: (X \/ Y) is compact by COMPTS_1: 10;

 then

 A3: ( S-max (X \/ Y)) in (X \/ Y) by SPRECT_1: 12;



 A4: ( S-max X) in X by SPRECT_1: 12;



 A5: (( S-max X) `2 ) = ( S-bound X) by EUCLID: 52;

 assume

 A6: ( S-bound X) < ( S-bound Y);

 then

 A7: ( S-bound (X \/ Y)) = ( S-bound X) by Th25;

 X c= (X \/ Y) by XBOOLE_1: 7;

 then ( S-max X) in ( S-most (X \/ Y)) by A2, A7, A5, A4, SPRECT_2: 11;

 then

 A8: (( S-max (X \/ Y)) `1 ) >= (( S-max X) `1 ) by A2, PSCOMP_1: 55;

 per cases by A3, XBOOLE_0:def 3;

 suppose ( S-max (X \/ Y)) in X;

 then ( S-max (X \/ Y)) in ( S-most X) by A6, A1, Th25, SPRECT_2: 11;

 then (( S-max (X \/ Y)) `1 ) <= (( S-max X) `1 ) by PSCOMP_1: 55;

 then (( S-max (X \/ Y)) `1 ) = (( S-max X) `1 ) by A8, XXREAL_0: 1;

 hence thesis by A6, A1, A5, Th25, TOPREAL3: 6;

 end;

 suppose ( S-max (X \/ Y)) in Y;

 hence thesis by A6, A7, A1, PSCOMP_1: 24;

 end;

 end;

 theorem :: JORDAN1J:33



 Th33: for X,Y be non empty compact Subset of ( TOP-REAL 2) st ( W-bound X) < ( W-bound Y) holds ( W-min (X \/ Y)) = ( W-min X)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);



 A1: (( W-min (X \/ Y)) `1 ) = ( W-bound (X \/ Y)) by EUCLID: 52;



 A2: (X \/ Y) is compact by COMPTS_1: 10;

 then

 A3: ( W-min (X \/ Y)) in (X \/ Y) by SPRECT_1: 13;



 A4: ( W-min X) in X by SPRECT_1: 13;



 A5: (( W-min X) `1 ) = ( W-bound X) by EUCLID: 52;

 assume

 A6: ( W-bound X) < ( W-bound Y);

 then

 A7: ( W-bound (X \/ Y)) = ( W-bound X) by Th26;

 X c= (X \/ Y) by XBOOLE_1: 7;

 then ( W-min X) in ( W-most (X \/ Y)) by A2, A7, A5, A4, SPRECT_2: 12;

 then

 A8: (( W-min (X \/ Y)) `2 ) <= (( W-min X) `2 ) by A2, PSCOMP_1: 31;

 per cases by A3, XBOOLE_0:def 3;

 suppose ( W-min (X \/ Y)) in X;

 then ( W-min (X \/ Y)) in ( W-most X) by A6, A1, Th26, SPRECT_2: 12;

 then (( W-min (X \/ Y)) `2 ) >= (( W-min X) `2 ) by PSCOMP_1: 31;

 then (( W-min (X \/ Y)) `2 ) = (( W-min X) `2 ) by A8, XXREAL_0: 1;

 hence thesis by A6, A1, A5, Th26, TOPREAL3: 6;

 end;

 suppose ( W-min (X \/ Y)) in Y;

 hence thesis by A6, A7, A1, PSCOMP_1: 24;

 end;

 end;

 theorem :: JORDAN1J:34

 for X,Y be non empty compact Subset of ( TOP-REAL 2) st ( W-bound X) < ( W-bound Y) holds ( W-max (X \/ Y)) = ( W-max X)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);



 A1: (( W-max (X \/ Y)) `1 ) = ( W-bound (X \/ Y)) by EUCLID: 52;



 A2: (X \/ Y) is compact by COMPTS_1: 10;

 then

 A3: ( W-max (X \/ Y)) in (X \/ Y) by SPRECT_1: 13;



 A4: ( W-max X) in X by SPRECT_1: 13;



 A5: (( W-max X) `1 ) = ( W-bound X) by EUCLID: 52;

 assume

 A6: ( W-bound X) < ( W-bound Y);

 then

 A7: ( W-bound (X \/ Y)) = ( W-bound X) by Th26;

 X c= (X \/ Y) by XBOOLE_1: 7;

 then ( W-max X) in ( W-most (X \/ Y)) by A2, A7, A5, A4, SPRECT_2: 12;

 then

 A8: (( W-max (X \/ Y)) `2 ) >= (( W-max X) `2 ) by A2, PSCOMP_1: 31;

 per cases by A3, XBOOLE_0:def 3;

 suppose ( W-max (X \/ Y)) in X;

 then ( W-max (X \/ Y)) in ( W-most X) by A6, A1, Th26, SPRECT_2: 12;

 then (( W-max (X \/ Y)) `2 ) <= (( W-max X) `2 ) by PSCOMP_1: 31;

 then (( W-max (X \/ Y)) `2 ) = (( W-max X) `2 ) by A8, XXREAL_0: 1;

 hence thesis by A6, A1, A5, Th26, TOPREAL3: 6;

 end;

 suppose ( W-max (X \/ Y)) in Y;

 hence thesis by A6, A7, A1, PSCOMP_1: 24;

 end;

 end;

 theorem :: JORDAN1J:35



 Th35: for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st f is being_S-Seq & p in ( L~ f) holds (( L_Cut (f,p)) /. ( len ( L_Cut (f,p)))) = (f /. ( len f))

 proof

 let f be FinSequence of ( TOP-REAL 2);

 let p be Point of ( TOP-REAL 2);

 assume that

 A1: f is being_S-Seq and

 A2: p in ( L~ f);



 A3: ( len f) in ( dom f) by A1, FINSEQ_5: 6;

 ( L_Cut (f,p)) <> {} by A2, JORDAN1E: 3;

 then ( len ( L_Cut (f,p))) in ( dom ( L_Cut (f,p))) by FINSEQ_5: 6;



 hence (( L_Cut (f,p)) /. ( len ( L_Cut (f,p)))) = (( L_Cut (f,p)) . ( len ( L_Cut (f,p)))) by PARTFUN1:def 6

 .= (f . ( len f)) by A1, A2, JORDAN1B: 4

 .= (f /. ( len f)) by A3, PARTFUN1:def 6;

 end;

 theorem :: JORDAN1J:36



 Th36: for f be non constant standard special_circular_sequence holds for p,q be Point of ( TOP-REAL 2) holds for g be connected Subset of ( TOP-REAL 2) st p in ( RightComp f) & q in ( LeftComp f) & p in g & q in g holds g meets ( L~ f)

 proof

 let f be non constant standard special_circular_sequence;

 let p,q be Point of ( TOP-REAL 2);

 let g be connected Subset of ( TOP-REAL 2);

 assume that

 A1: p in ( RightComp f) and

 A2: q in ( LeftComp f) and

 A3: p in g and

 A4: q in g;

 assume g misses ( L~ f);

 then g c= (( L~ f) ` ) by TDLAT_1: 2;

 then

 reconsider A = g as Subset of (( TOP-REAL 2) | (( L~ f) ` )) by PRE_TOPC: 8;

 ( RightComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 2;

 then

 consider R be Subset of (( TOP-REAL 2) | (( L~ f) ` )) such that

 A5: R = ( RightComp f) and

 A6: R is a_component by CONNSP_1:def 6;

 (R /\ A) <> {} by A1, A3, A5, XBOOLE_0:def 4;

 then

 A7: R meets A;

 ( LeftComp f) is_a_component_of (( L~ f) ` ) by GOBOARD9:def 1;

 then

 consider L be Subset of (( TOP-REAL 2) | (( L~ f) ` )) such that

 A8: L = ( LeftComp f) and

 A9: L is a_component by CONNSP_1:def 6;

 (L /\ A) <> {} by A2, A4, A8, XBOOLE_0:def 4;

 then

 A10: L meets A;

 A is connected by CONNSP_1: 23;

 hence contradiction by A5, A6, A8, A9, A7, A10, JORDAN2C: 92, SPRECT_4: 6;

 end;

 registration

 cluster non constant standard s.c.c. for being_S-Seq FinSequence of ( TOP-REAL 2);

 existence

 proof

 set n = the Nat;

 set C = the Simple_closed_curve;



 A1: ( Upper_Seq (C,n)) is_sequence_on ( Gauge (C,n)) by JORDAN1G: 4;

 take ( Upper_Seq (C,n));

 ( len ( Upper_Seq (C,n))) >= 2 by TOPREAL1:def 8;

 hence thesis by A1, JGRAPH_1: 12, JORDAN8: 5;

 end;

 end

 theorem :: JORDAN1J:37



 Th37: for f be S-Sequence_in_R2 holds for p be Point of ( TOP-REAL 2) st p in ( rng f) holds ( L_Cut (f,p)) = ( mid (f,(p .. f),( len f)))

 proof

 let f be S-Sequence_in_R2;

 let p be Point of ( TOP-REAL 2);



 A1: ( len f) >= 2 by TOPREAL1:def 8;

 assume p in ( rng f);

 then

 consider i be Nat such that

 A2: i in ( dom f) and

 A3: (f . i) = p by FINSEQ_2: 10;



 A4: ( 0 + 1) <= i by A2, FINSEQ_3: 25;



 A5: i <= ( len f) by A2, FINSEQ_3: 25;

 per cases by A4, XXREAL_0: 1;

 suppose i > 1;

 then

 A6: (( Index (p,f)) + 1) = i by A3, A5, JORDAN3: 12;

 then ( L_Cut (f,p)) = ( mid (f,(( Index (p,f)) + 1),( len f))) by A3, JORDAN3:def 3;

 hence thesis by A2, A3, A6, FINSEQ_5: 11;

 end;

 suppose

 A7: i = 1;



 thus ( L_Cut (f,p)) = ( L_Cut (f,(f /. i))) by A2, A3, PARTFUN1:def 6

 .= f by A7, JORDAN5B: 27

 .= ( mid (f,1,( len f))) by A1, FINSEQ_6: 120, XXREAL_0: 2

 .= ( mid (f,(p .. f),( len f))) by A2, A3, A7, FINSEQ_5: 11;

 end;

 end;

 theorem :: JORDAN1J:38



 Th38: for M be Go-board holds for f be S-Sequence_in_R2 st f is_sequence_on M holds for p be Point of ( TOP-REAL 2) st p in ( rng f) holds ( R_Cut (f,p)) is_sequence_on M

 proof

 let M be Go-board;

 let f be S-Sequence_in_R2;

 assume

 A1: f is_sequence_on M;

 let p be Point of ( TOP-REAL 2);

 assume p in ( rng f);

 then ( R_Cut (f,p)) = ( mid (f,1,(p .. f))) by JORDAN1G: 49;

 hence thesis by A1, JORDAN1H: 27;

 end;

 theorem :: JORDAN1J:39



 Th39: for M be Go-board holds for f be S-Sequence_in_R2 st f is_sequence_on M holds for p be Point of ( TOP-REAL 2) st p in ( rng f) holds ( L_Cut (f,p)) is_sequence_on M

 proof

 let M be Go-board;

 let f be S-Sequence_in_R2;

 assume

 A1: f is_sequence_on M;

 let p be Point of ( TOP-REAL 2);

 assume p in ( rng f);

 then ( L_Cut (f,p)) = ( mid (f,(p .. f),( len f))) by Th37;

 hence thesis by A1, JORDAN1H: 27;

 end;

 theorem :: JORDAN1J:40



 Th40: for G be Go-board holds for f be FinSequence of ( TOP-REAL 2) st f is_sequence_on G holds for i,j be Nat st 1 <= i & i <= ( len G) & 1 <= j & j <= ( width G) holds (G * (i,j)) in ( L~ f) implies (G * (i,j)) in ( rng f)

 proof

 let G be Go-board;

 let f be FinSequence of ( TOP-REAL 2);

 assume

 A1: f is_sequence_on G;

 let i,j be Nat;

 assume that

 A2: 1 <= i and

 A3: i <= ( len G) and

 A4: 1 <= j and

 A5: j <= ( width G);

 assume (G * (i,j)) in ( L~ f);

 then

 consider k be Nat such that

 A6: 1 <= k and

 A7: (k + 1) <= ( len f) and

 A8: (G * (i,j)) in ( LSeg ((f /. k),(f /. (k + 1)))) by SPPOL_2: 14;

 consider i1,j1,i2,j2 be Nat such that

 A9: [i1, j1] in ( Indices G) and

 A10: (f /. k) = (G * (i1,j1)) and

 A11: [i2, j2] in ( Indices G) and

 A12: (f /. (k + 1)) = (G * (i2,j2)) and

 A13: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A1, A6, A7, JORDAN8: 3;



 A14: 1 <= i1 by A9, MATRIX_0: 32;



 A15: 1 <= j2 by A11, MATRIX_0: 32;



 A16: i2 <= ( len G) by A11, MATRIX_0: 32;

 (k + 1) >= 1 by NAT_1: 11;

 then

 A17: (k + 1) in ( dom f) by A7, FINSEQ_3: 25;



 A18: 1 <= j1 by A9, MATRIX_0: 32;

 k < ( len f) by A7, NAT_1: 13;

 then

 A19: k in ( dom f) by A6, FINSEQ_3: 25;



 A20: i1 <= ( len G) by A9, MATRIX_0: 32;



 A21: j2 <= ( width G) by A11, MATRIX_0: 32;



 A22: 1 <= i2 by A11, MATRIX_0: 32;



 A23: j1 <= ( width G) by A9, MATRIX_0: 32;

 per cases by A13;

 suppose

 A24: i1 = i2 & (j1 + 1) = j2;

 j1 <= (j1 + 1) by NAT_1: 11;

 then

 A25: ((G * (i1,j1)) `2 ) <= ((G * (i1,(j1 + 1))) `2 ) by A14, A20, A18, A21, A24, JORDAN1A: 19;

 then ((G * (i1,j1)) `2 ) <= ((G * (i,j)) `2 ) by A8, A10, A12, A24, TOPREAL1: 4;

 then

 A26: j1 <= j by A2, A3, A4, A14, A20, A23, Th2;



 A27: ((G * (i1,j1)) `1 ) <= ((G * (i1,(j1 + 1))) `1 ) by A14, A20, A18, A23, A15, A21, A24, JORDAN1A: 18;

 then ((G * (i1,j1)) `1 ) <= ((G * (i,j)) `1 ) by A8, A10, A12, A24, TOPREAL1: 3;

 then

 A28: i1 <= i by A2, A4, A5, A20, A18, A23, Th1;

 ((G * (i,j)) `2 ) <= ((G * (i1,(j1 + 1))) `2 ) by A8, A10, A12, A24, A25, TOPREAL1: 4;

 then j <= (j1 + 1) by A2, A3, A5, A14, A20, A15, A24, Th2;

 then

 A29: j = j1 or j = (j1 + 1) by A26, NAT_1: 9;

 ((G * (i,j)) `1 ) <= ((G * (i1,(j1 + 1))) `1 ) by A8, A10, A12, A24, A27, TOPREAL1: 3;

 then i <= i1 by A3, A4, A5, A14, A15, A21, A24, Th1;

 then i = i1 by A28, XXREAL_0: 1;

 hence thesis by A10, A12, A19, A17, A24, A29, PARTFUN2: 2;

 end;

 suppose

 A30: (i1 + 1) = i2 & j1 = j2;

 i1 <= (i1 + 1) by NAT_1: 11;

 then

 A31: ((G * (i1,j1)) `1 ) <= ((G * ((i1 + 1),j1)) `1 ) by A14, A18, A23, A16, A30, JORDAN1A: 18;

 then ((G * (i1,j1)) `1 ) <= ((G * (i,j)) `1 ) by A8, A10, A12, A30, TOPREAL1: 3;

 then

 A32: i1 <= i by A2, A4, A5, A20, A18, A23, Th1;



 A33: ((G * (i1,j1)) `2 ) <= ((G * ((i1 + 1),j1)) `2 ) by A14, A20, A18, A23, A22, A16, A30, JORDAN1A: 19;

 then ((G * (i1,j1)) `2 ) <= ((G * (i,j)) `2 ) by A8, A10, A12, A30, TOPREAL1: 4;

 then

 A34: j1 <= j by A2, A3, A4, A14, A20, A23, Th2;

 ((G * (i,j)) `1 ) <= ((G * ((i1 + 1),j1)) `1 ) by A8, A10, A12, A30, A31, TOPREAL1: 3;

 then i <= (i1 + 1) by A3, A4, A5, A18, A23, A22, A30, Th1;

 then

 A35: i = i1 or i = (i1 + 1) by A32, NAT_1: 9;

 ((G * (i,j)) `2 ) <= ((G * ((i1 + 1),j1)) `2 ) by A8, A10, A12, A30, A33, TOPREAL1: 4;

 then j <= j1 by A2, A3, A5, A18, A22, A16, A30, Th2;

 then j = j1 by A34, XXREAL_0: 1;

 hence thesis by A10, A12, A19, A17, A30, A35, PARTFUN2: 2;

 end;

 suppose

 A36: i1 = (i2 + 1) & j1 = j2;

 i2 <= (i2 + 1) by NAT_1: 11;

 then

 A37: ((G * (i2,j1)) `1 ) <= ((G * ((i2 + 1),j1)) `1 ) by A20, A18, A23, A22, A36, JORDAN1A: 18;

 then ((G * (i2,j1)) `1 ) <= ((G * (i,j)) `1 ) by A8, A10, A12, A36, TOPREAL1: 3;

 then

 A38: i2 <= i by A2, A4, A5, A18, A23, A16, Th1;



 A39: ((G * (i2,j1)) `2 ) <= ((G * ((i2 + 1),j1)) `2 ) by A14, A20, A18, A23, A22, A16, A36, JORDAN1A: 19;

 then ((G * (i2,j1)) `2 ) <= ((G * (i,j)) `2 ) by A8, A10, A12, A36, TOPREAL1: 4;

 then

 A40: j1 <= j by A2, A3, A4, A23, A22, A16, Th2;

 ((G * (i,j)) `1 ) <= ((G * ((i2 + 1),j1)) `1 ) by A8, A10, A12, A36, A37, TOPREAL1: 3;

 then i <= (i2 + 1) by A3, A4, A5, A14, A18, A23, A36, Th1;

 then

 A41: i = i2 or i = (i2 + 1) by A38, NAT_1: 9;

 ((G * (i,j)) `2 ) <= ((G * ((i2 + 1),j1)) `2 ) by A8, A10, A12, A36, A39, TOPREAL1: 4;

 then j <= j1 by A2, A3, A5, A14, A20, A18, A36, Th2;

 then j = j1 by A40, XXREAL_0: 1;

 hence thesis by A10, A12, A19, A17, A36, A41, PARTFUN2: 2;

 end;

 suppose

 A42: i1 = i2 & j1 = (j2 + 1);

 j2 <= (j2 + 1) by NAT_1: 11;

 then

 A43: ((G * (i1,j2)) `2 ) <= ((G * (i1,(j2 + 1))) `2 ) by A14, A20, A23, A15, A42, JORDAN1A: 19;

 then ((G * (i1,j2)) `2 ) <= ((G * (i,j)) `2 ) by A8, A10, A12, A42, TOPREAL1: 4;

 then

 A44: j2 <= j by A2, A3, A4, A14, A20, A21, Th2;



 A45: ((G * (i1,j2)) `1 ) <= ((G * (i1,(j2 + 1))) `1 ) by A14, A20, A18, A23, A15, A21, A42, JORDAN1A: 18;

 then ((G * (i1,j2)) `1 ) <= ((G * (i,j)) `1 ) by A8, A10, A12, A42, TOPREAL1: 3;

 then

 A46: i1 <= i by A2, A4, A5, A20, A15, A21, Th1;

 ((G * (i,j)) `2 ) <= ((G * (i1,(j2 + 1))) `2 ) by A8, A10, A12, A42, A43, TOPREAL1: 4;

 then j <= (j2 + 1) by A2, A3, A5, A14, A20, A18, A42, Th2;

 then

 A47: j = j2 or j = (j2 + 1) by A44, NAT_1: 9;

 ((G * (i,j)) `1 ) <= ((G * (i1,(j2 + 1))) `1 ) by A8, A10, A12, A42, A45, TOPREAL1: 3;

 then i <= i1 by A3, A4, A5, A14, A18, A23, A42, Th1;

 then i = i1 by A46, XXREAL_0: 1;

 hence thesis by A10, A12, A19, A17, A42, A47, PARTFUN2: 2;

 end;

 end;

 theorem :: JORDAN1J:41

 for f be S-Sequence_in_R2 holds for g be FinSequence of ( TOP-REAL 2) holds g is unfolded s.n.c. one-to-one & (( L~ f) /\ ( L~ g)) = {(f /. 1)} & (f /. 1) = (g /. ( len g)) & (for i be Nat st 1 <= i & (i + 2) <= ( len f) holds (( LSeg (f,i)) /\ ( LSeg ((f /. ( len f)),(g /. 1)))) = {} ) & (for i be Nat st 2 <= i & (i + 1) <= ( len g) holds (( LSeg (g,i)) /\ ( LSeg ((f /. ( len f)),(g /. 1)))) = {} ) implies (f ^ g) is s.c.c.

 proof

 let f be S-Sequence_in_R2;

 let g be FinSequence of ( TOP-REAL 2);

 assume that

 A1: g is unfolded s.n.c. one-to-one and

 A2: (( L~ f) /\ ( L~ g)) = {(f /. 1)} and

 A3: (f /. 1) = (g /. ( len g)) and

 A4: for i be Nat st 1 <= i & (i + 2) <= ( len f) holds (( LSeg (f,i)) /\ ( LSeg ((f /. ( len f)),(g /. 1)))) = {} and

 A5: for i be Nat st 2 <= i & (i + 1) <= ( len g) holds (( LSeg (g,i)) /\ ( LSeg ((f /. ( len f)),(g /. 1)))) = {} ;

 let i,j be Nat such that

 A6: (i + 1) < j and

 A7: i > 1 & j < ( len (f ^ g)) or (j + 1) < ( len (f ^ g));



 A8: (j + 1) <= ( len (f ^ g)) by A7, NAT_1: 13;



 A9: for i be Nat st 2 <= i & (i + 1) <= ( len g) holds ( LSeg (g,i)) misses ( LSeg ((f /. ( len f)),(g /. 1))) by A5;



 A10: for i be Nat st 1 <= i & (i + 2) <= ( len f) holds ( LSeg (f,i)) misses ( LSeg ((f /. ( len f)),(g /. 1))) by A4;

 per cases ;

 suppose i = 0 ;

 then ( LSeg ((f ^ g),i)) = {} by TOPREAL1:def 3;

 then (( LSeg ((f ^ g),i)) /\ ( LSeg ((f ^ g),j))) = {} ;

 hence thesis;

 end;

 suppose

 A11: i <> 0 ;



 A12: ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22;

 i <= (i + 1) by NAT_1: 11;

 then

 A13: i < j by A6, XXREAL_0: 2;

 now

 per cases ;

 suppose

 A14: (j + 1) <= ( len f);

 j <= (j + 1) by NAT_1: 11;

 then i < (j + 1) by A13, XXREAL_0: 2;

 then i < ( len f) by A14, XXREAL_0: 2;

 then (i + 1) <= ( len f) by NAT_1: 13;

 then

 A15: ( LSeg ((f ^ g),i)) = ( LSeg (f,i)) by SPPOL_2: 6;

 ( LSeg ((f ^ g),j)) = ( LSeg (f,j)) by A14, SPPOL_2: 6;

 hence thesis by A6, A15, TOPREAL1:def 7;

 end;

 suppose (j + 1) > ( len f);

 then

 A16: ( len f) <= j by NAT_1: 13;

 then

 reconsider j9 = (j - ( len f)) as Element of NAT by INT_1: 5;



 A17: ((j + 1) - ( len f)) <= ( len g) by A8, A12, XREAL_1: 20;

 then

 A18: (j9 + 1) <= ( len g);



 A19: (( len f) + j9) = j;

 now

 per cases ;

 suppose

 A20: i <= ( len f);

 now

 per cases ;

 suppose

 A21: i = ( len f);

 g is non empty by A18;

 then

 A22: ( LSeg ((f ^ g),i)) = ( LSeg ((f /. ( len f)),(g /. 1))) by A21, SPPOL_2: 8;

 ((( len f) + 1) + 1) <= j by A6, A21, NAT_1: 13;

 then (( len f) + (1 + 1)) <= j;

 then

 A23: (1 + 1) <= j9 by XREAL_1: 19;

 then ( LSeg ((f ^ g),j)) = ( LSeg (g,j9)) by A19, SPPOL_2: 7, XXREAL_0: 2;

 hence thesis by A9, A18, A23, A22;

 end;

 suppose i <> ( len f);

 then i < ( len f) by A20, XXREAL_0: 1;

 then (i + 1) <= ( len f) by NAT_1: 13;

 then

 A24: ( LSeg ((f ^ g),i)) = ( LSeg (f,i)) by SPPOL_2: 6;

 now

 per cases ;

 suppose

 A25: j = ( len f);

 then ((i + 1) + 1) <= ( len f) by A6, NAT_1: 13;

 then

 A26: (i + (1 + 1)) <= ( len f);

 g is non empty by A8, A12, A25, XREAL_1: 6;

 then ( LSeg ((f ^ g),j)) = ( LSeg ((f /. ( len f)),(g /. 1))) by A25, SPPOL_2: 8;

 hence thesis by A10, A11, A24, A26, NAT_1: 14;

 end;

 suppose

 A27: j <> ( len f);



 A28: ( len f) >= 2 by TOPREAL1:def 8;



 A29: ( LSeg ((f ^ g),i)) c= ( L~ f) by A24, TOPREAL3: 19;

 ( len f) < j by A16, A27, XXREAL_0: 1;

 then (( len f) + 1) <= j by NAT_1: 13;

 then

 A30: 1 <= j9 by XREAL_1: 19;

 then

 A31: ( LSeg ((f ^ g),(( len f) + j9))) = ( LSeg (g,j9)) by SPPOL_2: 7;

 then ( LSeg ((f ^ g),j)) c= ( L~ g) by TOPREAL3: 19;

 then

 A32: (( LSeg ((f ^ g),i)) /\ ( LSeg ((f ^ g),j))) c= {(f /. 1)} by A2, A29, XBOOLE_1: 27;

 now

 per cases by A32, ZFMISC_1: 33;

 suppose (( LSeg ((f ^ g),i)) /\ ( LSeg ((f ^ g),j))) = {} ;

 hence thesis;

 end;

 suppose (( LSeg ((f ^ g),i)) /\ ( LSeg ((f ^ g),j))) = {(f /. 1)};

 then

 A33: (f /. 1) in (( LSeg ((f ^ g),i)) /\ ( LSeg ((f ^ g),j))) by TARSKI:def 1;

 then

 A34: (f /. 1) in ( LSeg ((f ^ g),i)) by XBOOLE_0:def 4;

 j9 < ( len g) by A18, NAT_1: 13;

 then

 A35: j9 in ( dom g) by A30, FINSEQ_3: 25;

 (j9 + 1) >= 1 by NAT_1: 11;

 then

 A36: (j9 + 1) in ( dom g) by A17, FINSEQ_3: 25;

 (f /. 1) in ( LSeg ((f ^ g),j)) by A33, XBOOLE_0:def 4;

 then (j9 + 1) = ( len g) by A1, A3, A31, A35, A36, GOBOARD2: 2;

 hence thesis by A7, A12, A24, A28, A34, JORDAN5B: 30;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 suppose

 A37: i > ( len f);

 then j <> ( len f) by A6, NAT_1: 13;

 then ( len f) < j by A16, XXREAL_0: 1;

 then (( len f) + 1) <= j by NAT_1: 13;

 then 1 <= j9 by XREAL_1: 19;

 then

 A38: ( LSeg ((f ^ g),(( len f) + j9))) = ( LSeg (g,j9)) by SPPOL_2: 7;

 reconsider i9 = (i - ( len f)) as Element of NAT by A37, INT_1: 5;

 (( len f) + 1) <= i by A37, NAT_1: 13;

 then 1 <= i9 by XREAL_1: 19;

 then

 A39: ( LSeg ((f ^ g),(( len f) + i9))) = ( LSeg (g,i9)) by SPPOL_2: 7;

 ((i + 1) - ( len f)) < j9 by A6, XREAL_1: 9;

 then (i9 + 1) < j9;

 hence thesis by A1, A39, A38, TOPREAL1:def 7;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 end;

 theorem :: JORDAN1J:42

 for C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2) holds ex i be Nat st 1 <= i & (i + 1) <= ( len ( Gauge (C,n))) & ( W-min C) in ( cell (( Gauge (C,n)),1,i)) & ( W-min C) <> (( Gauge (C,n)) * (2,i))

 proof

 let C be compact non vertical non horizontal non empty Subset of ( TOP-REAL 2);

 set G = ( Gauge (C,n));

 defpred P[ Nat] means 1 <= $1 & $1 < ( len G) & ((G * (2,$1)) `2 ) < (( W-min C) `2 );



 A1: for k be Nat st P[k] holds k <= ( len G);



 A2: ( len G) = ( width G) by JORDAN8:def 1;

 (( SW-corner C) `2 ) <= (( W-min C) `2 ) by PSCOMP_1: 30;

 then

 A3: ( S-bound C) <= (( W-min C) `2 ) by EUCLID: 52;



 A4: ( len G) >= 4 by JORDAN8: 10;

 then

 A5: 1 < ( len G) by XXREAL_0: 2;



 A6: 2 <= ( len G) by A4, XXREAL_0: 2;

 then ((G * (2,2)) `2 ) = ( S-bound C) by JORDAN8: 13;

 then ((G * (2,1)) `2 ) < ( S-bound C) by A2, A6, GOBOARD5: 4;

 then ((G * (2,1)) `2 ) < (( W-min C) `2 ) by A3, XXREAL_0: 2;

 then

 A7: ex k be Nat st P[k] by A5;

 ex i be Nat st P[i] & for n be Nat st P[n] holds n <= i from NAT_1:sch 6( A1, A7);

 then

 consider i be Nat such that

 A8: 1 <= i and

 A9: i < ( len G) and

 A10: ((G * (2,i)) `2 ) < (( W-min C) `2 ) and

 A11: for n be Nat st P[n] holds n <= i;

 reconsider i as Nat;



 A12: (( W-min C) `1 ) = ( W-bound C) by EUCLID: 52;

 then

 A13: ((G * (2,i)) `1 ) = (( W-min C) `1 ) by A8, A9, JORDAN8: 11;



 A14: (i + 1) <= ( len G) by A9, NAT_1: 13;

 then

 A15: (( W-min C) `1 ) = ((G * (2,(i + 1))) `1 ) by A12, JORDAN8: 11, NAT_1: 12;



 A16: i < (i + 1) by NAT_1: 13;



 A17: 1 <= (i + 1) by NAT_1: 12;

 now

 assume (i + 1) = ( len G);

 then (( len G) -' 1) = i by NAT_D: 34;

 then

 A18: ((G * (2,i)) `2 ) = ( N-bound C) by A6, JORDAN8: 14;

 (( NW-corner C) `2 ) >= (( W-min C) `2 ) by PSCOMP_1: 30;

 hence contradiction by A10, A18, EUCLID: 52;

 end;

 then (i + 1) < ( len G) by A14, XXREAL_0: 1;

 then (( W-min C) `2 ) <= ((G * (2,(i + 1))) `2 ) by A11, A17, A16;

 then

 A19: ( W-min C) in ( LSeg ((G * (2,i)),(G * (2,(i + 1))))) by A10, A13, A15, GOBOARD7: 7;

 take i;

 thus 1 <= i & (i + 1) <= ( len G) by A8, A9, NAT_1: 13;

 ( len G) = ( width G) by JORDAN8:def 1;

 then ( LSeg ((G * ((1 + 1),i)),(G * ((1 + 1),(i + 1))))) c= ( cell (G,1,i)) by A5, A8, A9, GOBOARD5: 18;

 hence ( W-min C) in ( cell (G,1,i)) by A19;

 thus thesis by A10;

 end;

 theorem :: JORDAN1J:43



 Th43: for f be S-Sequence_in_R2 holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) & (f . ( len f)) in ( L~ ( R_Cut (f,p))) holds (f . ( len f)) = p

 proof

 let f be S-Sequence_in_R2;

 let p be Point of ( TOP-REAL 2);

 assume that

 A1: p in ( L~ f) and

 A2: (f . ( len f)) in ( L~ ( R_Cut (f,p)));



 A3: ( L~ f) = ( L~ ( Rev f)) by SPPOL_2: 22;



 A4: (( Rev f) . 1) = (f . ( len f)) by FINSEQ_5: 62;

 ( L_Cut (( Rev f),p)) = ( Rev ( R_Cut (f,p))) by A1, JORDAN3: 22;

 then (( Rev f) . 1) in ( L~ ( L_Cut (( Rev f),p))) by A2, A4, SPPOL_2: 22;

 hence thesis by A1, A3, A4, JORDAN1E: 7;

 end;

 theorem :: JORDAN1J:44



 Th44: for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) holds ( R_Cut (f,p)) <> {}

 proof

 let f be FinSequence of ( TOP-REAL 2);

 let p be Point of ( TOP-REAL 2);

 per cases ;

 suppose p <> (f . 1);

 then ( R_Cut (f,p)) = (( mid (f,1,( Index (p,f)))) ^ <*p*>) by JORDAN3:def 4;

 hence thesis;

 end;

 suppose p = (f . 1);

 then ( R_Cut (f,p)) = <*p*> by JORDAN3:def 4;

 hence thesis;

 end;

 end;

 theorem :: JORDAN1J:45



 Th45: for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) holds (( R_Cut (f,p)) /. ( len ( R_Cut (f,p)))) = p

 proof

 let f be FinSequence of ( TOP-REAL 2);

 let p be Point of ( TOP-REAL 2);

 assume

 A1: p in ( L~ f);

 ( R_Cut (f,p)) is non empty by Th44;

 then ( len ( R_Cut (f,p))) in ( dom ( R_Cut (f,p))) by FINSEQ_5: 6;



 hence (( R_Cut (f,p)) /. ( len ( R_Cut (f,p)))) = (( R_Cut (f,p)) . ( len ( R_Cut (f,p)))) by PARTFUN1:def 6

 .= p by A1, JORDAN3: 24;

 end;

 theorem :: JORDAN1J:46



 Th46: for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) holds p in ( L~ ( Upper_Seq (C,n))) & (p `1 ) = ( E-bound ( L~ ( Cage (C,n)))) implies p = ( E-max ( L~ ( Cage (C,n))))

 proof

 let C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2);

 let p be Point of ( TOP-REAL 2);

 set Ca = ( Cage (C,n));

 set US = ( Upper_Seq (C,n));

 set LS = ( Lower_Seq (C,n));

 set Wmin = ( W-min ( L~ Ca));

 set Smax = ( S-max ( L~ Ca));

 set Smin = ( S-min ( L~ Ca));

 set Emin = ( E-min ( L~ Ca));

 set Emax = ( E-max ( L~ Ca));

 set Wbo = ( W-bound ( L~ ( Cage (C,n))));

 set Nbo = ( N-bound ( L~ ( Cage (C,n))));

 set Ebo = ( E-bound ( L~ ( Cage (C,n))));

 set Sbo = ( S-bound ( L~ ( Cage (C,n))));

 set NE = ( NE-corner ( L~ Ca));

 assume that

 A1: p in ( L~ ( Upper_Seq (C,n))) and

 A2: (p `1 ) = ( E-bound ( L~ ( Cage (C,n)))) and

 A3: p <> ( E-max ( L~ ( Cage (C,n))));



 A4: (US /. 1) = Wmin by JORDAN1F: 5;

 1 in ( dom US) by FINSEQ_5: 6;

 then

 A5: (US . 1) = Wmin by A4, PARTFUN1:def 6;

 Wbo <> Ebo by SPRECT_1: 31;

 then p <> (US . 1) by A2, A5, EUCLID: 52;

 then

 reconsider g = ( R_Cut (US,p)) as being_S-Seq FinSequence of ( TOP-REAL 2) by A1, JORDAN3: 35;

 <*p*> is_in_the_area_of Ca by A1, JORDAN1E: 17, SPRECT_3: 46;

 then

 A6: g is_in_the_area_of Ca by A1, JORDAN1E: 17, SPRECT_3: 52;

 ( len g) in ( dom g) by FINSEQ_5: 6;



 then

 A7: (g /. ( len g)) = (g . ( len g)) by PARTFUN1:def 6

 .= p by A1, JORDAN3: 24;

 ((g /. 1) `1 ) = ((US /. 1) `1 ) by A1, SPRECT_3: 22

 .= (Wmin `1 ) by JORDAN1F: 5

 .= Wbo by EUCLID: 52;

 then

 A8: g is_a_h.c._for Ca by A2, A6, A7, SPRECT_2:def 2;



 A9: (LS /. 1) = Emax by JORDAN1F: 6;

 1 in ( dom LS) by FINSEQ_5: 6;

 then

 A10: (LS . 1) = Emax by A9, PARTFUN1:def 6;

 ( len ( Cage (C,n))) > 4 by GOBOARD7: 34;

 then

 A11: ( rng ( Cage (C,n))) c= ( L~ ( Cage (C,n))) by SPPOL_2: 18, XXREAL_0: 2;

 now

 per cases ;

 suppose

 A12: Emax <> NE;



 A13: not NE in ( rng ( Cage (C,n)))

 proof



 A14: (NE `1 ) = ( E-bound ( L~ ( Cage (C,n)))) by EUCLID: 52;



 A15: (NE `2 ) = ( N-bound ( L~ ( Cage (C,n)))) by EUCLID: 52;

 then (NE `2 ) >= ( S-bound ( L~ ( Cage (C,n)))) by SPRECT_1: 22;

 then NE in { p1 where p1 be Point of ( TOP-REAL 2) : (p1 `1 ) = ( E-bound ( L~ ( Cage (C,n)))) & (p1 `2 ) <= ( N-bound ( L~ ( Cage (C,n)))) & (p1 `2 ) >= ( S-bound ( L~ ( Cage (C,n)))) } by A14, A15;

 then

 A16: NE in ( LSeg (( SE-corner ( L~ ( Cage (C,n)))),( NE-corner ( L~ ( Cage (C,n)))))) by SPRECT_1: 23;

 assume NE in ( rng ( Cage (C,n)));

 then NE in (( LSeg (( SE-corner ( L~ ( Cage (C,n)))),( NE-corner ( L~ ( Cage (C,n)))))) /\ ( L~ ( Cage (C,n)))) by A11, A16, XBOOLE_0:def 4;

 then

 A17: (NE `2 ) <= (( E-max ( L~ ( Cage (C,n)))) `2 ) by PSCOMP_1: 47;



 A18: (( E-max ( L~ ( Cage (C,n)))) `1 ) = (NE `1 ) by PSCOMP_1: 45;

 (( E-max ( L~ ( Cage (C,n)))) `2 ) <= (NE `2 ) by PSCOMP_1: 46;

 then (( E-max ( L~ ( Cage (C,n)))) `2 ) = (NE `2 ) by A17, XXREAL_0: 1;

 hence contradiction by A12, A18, TOPREAL3: 6;

 end;

 Smax in ( rng LS) by Th12;

 then ( R_Cut (LS,Smax)) = ( mid (LS,1,(Smax .. LS))) by JORDAN1G: 49;

 then

 A19: ( rng ( R_Cut (LS,Smax))) c= ( rng LS) by FINSEQ_6: 119;

 ( rng LS) c= ( rng Ca) by JORDAN1G: 39;

 then ( rng ( R_Cut (LS,Smax))) c= ( rng Ca) by A19;

 then not NE in ( rng ( R_Cut (LS,Smax))) by A13;

 then ( rng ( R_Cut (LS,Smax))) misses {NE} by ZFMISC_1: 50;

 then ( rng ( R_Cut (LS,Smax))) misses ( rng <*NE*>) by FINSEQ_1: 38;

 then

 A20: ( rng ( Rev ( R_Cut (LS,Smax)))) misses ( rng <*NE*>) by FINSEQ_5: 57;

 set h = (( Rev ( R_Cut (LS,Smax))) ^ <*NE*>);



 A21: <*NE*> is one-to-one by FINSEQ_3: 93;



 A22: ((h /. ( len h)) `2 ) = ((h /. (( len ( Rev ( R_Cut (LS,Smax)))) + 1)) `2 ) by FINSEQ_2: 16

 .= (NE `2 ) by FINSEQ_4: 67

 .= Nbo by EUCLID: 52;

 Emin in ( L~ Ca) by SPRECT_1: 14;

 then

 A23: Sbo <= (Emin `2 ) by PSCOMP_1: 24;



 A24: (( Index (Smax,LS)) + 1) >= ( 0 + 1) by XREAL_1: 7;



 A25: Smax in ( L~ LS) by Th12;

 then <*Smax*> is_in_the_area_of Ca by JORDAN1E: 18, SPRECT_3: 46;

 then ( R_Cut (LS,Smax)) is_in_the_area_of Ca by A25, JORDAN1E: 18, SPRECT_3: 52;

 then

 A26: ( Rev ( R_Cut (LS,Smax))) is_in_the_area_of Ca by SPRECT_3: 51;

 (Emin `2 ) < (Emax `2 ) by SPRECT_2: 53;

 then

 A27: Smax <> (LS . 1) by A10, A23, EUCLID: 52;

 then

 reconsider RCutLS = ( R_Cut (LS,Smax)) as being_S-Seq FinSequence of ( TOP-REAL 2) by A25, JORDAN3: 35;

 ( len h) = (( len ( Rev ( R_Cut (LS,Smax)))) + 1) by FINSEQ_2: 16

 .= (( len ( R_Cut (LS,Smax))) + 1) by FINSEQ_5:def 3

 .= ((( Index (Smax,LS)) + 1) + 1) by A25, A27, JORDAN3: 25;

 then

 A28: ( len h) >= (1 + 1) by A24, XREAL_1: 7;



 A29: 2 <= ( len g) by TOPREAL1:def 8;

 1 in ( dom ( Rev RCutLS)) by FINSEQ_5: 6;



 then (h /. 1) = (( Rev RCutLS) /. 1) by FINSEQ_4: 68

 .= (( R_Cut (LS,Smax)) /. ( len ( R_Cut (LS,Smax)))) by FINSEQ_5: 65

 .= Smax by A25, Th45;

 then

 A30: ((h /. 1) `2 ) = Sbo by EUCLID: 52;

 <*NE*> is_in_the_area_of Ca by SPRECT_2: 25;

 then h is_in_the_area_of Ca by A26, SPRECT_2: 24;

 then

 A31: h is_a_v.c._for Ca by A30, A22, SPRECT_2:def 3;



 A32: ( len LS) in ( dom LS) by FINSEQ_5: 6;



 A33: (( Rev RCutLS) /. ( len ( Rev RCutLS))) = (( Rev RCutLS) /. ( len RCutLS)) by FINSEQ_5:def 3

 .= (RCutLS /. 1) by FINSEQ_5: 65

 .= (LS /. 1) by A25, SPRECT_3: 22

 .= Emax by JORDAN1F: 6;



 then ((( Rev RCutLS) /. ( len ( Rev RCutLS))) `1 ) = ( E-bound ( L~ Ca)) by EUCLID: 52

 .= (NE `1 ) by EUCLID: 52

 .= (( <*NE*> /. 1) `1 ) by FINSEQ_4: 16;

 then h is one-to-one special by A20, A21, FINSEQ_3: 91, GOBOARD2: 8;

 then ( L~ g) meets ( L~ h) by A8, A29, A28, A31, SPRECT_2: 29;

 then

 consider x be object such that

 A34: x in ( L~ g) and

 A35: x in ( L~ h) by XBOOLE_0: 3;

 reconsider x as Point of ( TOP-REAL 2) by A34;



 A36: ( L~ h) = (( L~ ( Rev RCutLS)) \/ ( LSeg ((( Rev RCutLS) /. ( len ( Rev RCutLS))),NE))) by SPPOL_2: 19;



 A37: ( L~ RCutLS) c= ( L~ LS) by Th12, JORDAN3: 41;



 A38: ( len US) in ( dom US) by FINSEQ_5: 6;



 A39: ( L~ g) c= ( L~ US) by A1, JORDAN3: 41;

 then

 A40: x in ( L~ US) by A34;

 now

 per cases by A35, A36, XBOOLE_0:def 3;

 suppose x in ( L~ ( Rev RCutLS));

 then

 A41: x in ( L~ RCutLS) by SPPOL_2: 22;

 then x in (( L~ US) /\ ( L~ LS)) by A34, A39, A37, XBOOLE_0:def 4;

 then

 A42: x in {Wmin, Emax} by JORDAN1E: 16;

 now

 per cases by A42, TARSKI:def 2;

 suppose x = Wmin;

 then (LS /. ( len LS)) in ( L~ ( R_Cut (LS,Smax))) by A41, JORDAN1F: 8;

 then (LS . ( len LS)) in ( L~ ( R_Cut (LS,Smax))) by A32, PARTFUN1:def 6;

 then (LS . ( len LS)) = Smax by A25, Th43;

 then (LS /. ( len LS)) = Smax by A32, PARTFUN1:def 6;

 then

 A43: Wmin = Smax by JORDAN1F: 8;

 Smin in ( L~ Ca) by SPRECT_1: 12;

 then

 A44: Wbo <= (Smin `1 ) by PSCOMP_1: 24;

 (Smin `1 ) < (Smax `1 ) by SPRECT_2: 55;

 hence contradiction by A43, A44, EUCLID: 52;

 end;

 suppose x = Emax;

 then (US /. ( len US)) in ( L~ ( R_Cut (US,p))) by A34, JORDAN1F: 7;

 then (US . ( len US)) in ( L~ ( R_Cut (US,p))) by A38, PARTFUN1:def 6;

 then (US . ( len US)) = p by A1, Th43;

 then (US /. ( len US)) = p by A38, PARTFUN1:def 6;

 hence contradiction by A3, JORDAN1F: 7;

 end;

 end;

 hence contradiction;

 end;

 suppose

 A45: x in ( LSeg ((( Rev RCutLS) /. ( len ( Rev RCutLS))),NE));

 (Emax `2 ) <= (NE `2 ) by PSCOMP_1: 46;

 then

 A46: (Emax `2 ) <= (x `2 ) by A33, A45, TOPREAL1: 4;



 A47: (Emax `1 ) = Ebo by EUCLID: 52;

 (NE `1 ) = Ebo by EUCLID: 52;

 then

 A48: (x `1 ) = Ebo by A33, A45, A47, GOBOARD7: 5;

 ( L~ Ca) = (( L~ US) \/ ( L~ LS)) by JORDAN1E: 13;

 then ( L~ US) c= ( L~ Ca) by XBOOLE_1: 7;

 then x in ( E-most ( L~ Ca)) by A40, A48, SPRECT_2: 13;

 then (x `2 ) <= (Emax `2 ) by PSCOMP_1: 47;

 then (x `2 ) = (Emax `2 ) by A46, XXREAL_0: 1;

 then x = Emax by A47, A48, TOPREAL3: 6;

 then (US /. ( len US)) in ( L~ ( R_Cut (US,p))) by A34, JORDAN1F: 7;

 then (US . ( len US)) in ( L~ ( R_Cut (US,p))) by A38, PARTFUN1:def 6;

 then (US . ( len US)) = p by A1, Th43;

 then (US /. ( len US)) = p by A38, PARTFUN1:def 6;

 hence contradiction by A3, JORDAN1F: 7;

 end;

 end;

 hence contradiction;

 end;

 suppose

 A49: Emax = NE;

 Emin in ( L~ Ca) by SPRECT_1: 14;

 then

 A50: Sbo <= (Emin `2 ) by PSCOMP_1: 24;

 set h = ( Rev ( R_Cut (LS,Smax)));



 A51: 2 <= ( len g) by TOPREAL1:def 8;



 A52: Smax in ( L~ LS) by Th12;

 then <*Smax*> is_in_the_area_of Ca by JORDAN1E: 18, SPRECT_3: 46;

 then ( R_Cut (LS,Smax)) is_in_the_area_of Ca by A52, JORDAN1E: 18, SPRECT_3: 52;

 then

 A53: h is_in_the_area_of Ca by SPRECT_3: 51;

 (Emin `2 ) < (Emax `2 ) by SPRECT_2: 53;

 then Smax <> (LS . 1) by A10, A50, EUCLID: 52;

 then

 reconsider RCutLS = ( R_Cut (LS,Smax)) as being_S-Seq FinSequence of ( TOP-REAL 2) by A52, JORDAN3: 35;

 1 in ( dom ( Rev RCutLS)) by FINSEQ_5: 6;



 then (h /. 1) = (( R_Cut (LS,Smax)) /. ( len ( R_Cut (LS,Smax)))) by FINSEQ_5: 65

 .= Smax by A52, Th45;

 then

 A54: ((h /. 1) `2 ) = Sbo by EUCLID: 52;



 A55: ( Rev RCutLS) is special;

 ( len RCutLS) >= 2 by TOPREAL1:def 8;

 then

 A56: ( len h) >= 2 by FINSEQ_5:def 3;

 (( Rev RCutLS) /. ( len ( Rev RCutLS))) = (( Rev RCutLS) /. ( len RCutLS)) by FINSEQ_5:def 3

 .= (RCutLS /. 1) by FINSEQ_5: 65

 .= (LS /. 1) by A52, SPRECT_3: 22

 .= Emax by JORDAN1F: 6;

 then ((h /. ( len h)) `2 ) = Nbo by A49, EUCLID: 52;

 then h is_a_v.c._for Ca by A53, A54, SPRECT_2:def 3;

 then ( L~ g) meets ( L~ h) by A8, A55, A51, A56, SPRECT_2: 29;

 then

 consider x be object such that

 A57: x in ( L~ g) and

 A58: x in ( L~ h) by XBOOLE_0: 3;

 reconsider x as Point of ( TOP-REAL 2) by A57;



 A59: x in ( L~ RCutLS) by A58, SPPOL_2: 22;



 A60: ( L~ g) c= ( L~ US) by A1, JORDAN3: 41;



 A61: ( len US) in ( dom US) by FINSEQ_5: 6;



 A62: ( len LS) in ( dom LS) by FINSEQ_5: 6;

 ( L~ RCutLS) c= ( L~ LS) by Th12, JORDAN3: 41;

 then x in (( L~ US) /\ ( L~ LS)) by A57, A60, A59, XBOOLE_0:def 4;

 then

 A63: x in {Wmin, Emax} by JORDAN1E: 16;

 now

 per cases by A63, TARSKI:def 2;

 suppose x = Wmin;

 then (LS /. ( len LS)) in ( L~ ( R_Cut (LS,Smax))) by A59, JORDAN1F: 8;

 then (LS . ( len LS)) in ( L~ ( R_Cut (LS,Smax))) by A62, PARTFUN1:def 6;

 then (LS . ( len LS)) = Smax by A52, Th43;

 then (LS /. ( len LS)) = Smax by A62, PARTFUN1:def 6;

 then

 A64: Wmin = Smax by JORDAN1F: 8;

 Smin in ( L~ Ca) by SPRECT_1: 12;

 then

 A65: Wbo <= (Smin `1 ) by PSCOMP_1: 24;

 (Smin `1 ) < (Smax `1 ) by SPRECT_2: 55;

 hence contradiction by A64, A65, EUCLID: 52;

 end;

 suppose x = Emax;

 then (US /. ( len US)) in ( L~ ( R_Cut (US,p))) by A57, JORDAN1F: 7;

 then (US . ( len US)) in ( L~ ( R_Cut (US,p))) by A61, PARTFUN1:def 6;

 then (US . ( len US)) = p by A1, Th43;

 then (US /. ( len US)) = p by A61, PARTFUN1:def 6;

 hence contradiction by A3, JORDAN1F: 7;

 end;

 end;

 hence contradiction;

 end;

 end;

 hence contradiction;

 end;

 theorem :: JORDAN1J:47

 for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) holds p in ( L~ ( Lower_Seq (C,n))) & (p `1 ) = ( W-bound ( L~ ( Cage (C,n)))) implies p = ( W-min ( L~ ( Cage (C,n))))

 proof

 let C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2);

 let p be Point of ( TOP-REAL 2);

 set Ca = ( Cage (C,n));

 set LS = ( Lower_Seq (C,n));

 set US = ( Upper_Seq (C,n));

 set Emax = ( E-max ( L~ Ca));

 set Nmin = ( N-min ( L~ Ca));

 set Nmax = ( N-max ( L~ Ca));

 set Wmax = ( W-max ( L~ Ca));

 set Wmin = ( W-min ( L~ Ca));

 set Ebo = ( E-bound ( L~ ( Cage (C,n))));

 set Sbo = ( S-bound ( L~ ( Cage (C,n))));

 set Wbo = ( W-bound ( L~ ( Cage (C,n))));

 set Nbo = ( N-bound ( L~ ( Cage (C,n))));

 set SW = ( SW-corner ( L~ Ca));

 assume that

 A1: p in ( L~ ( Lower_Seq (C,n))) and

 A2: (p `1 ) = ( W-bound ( L~ ( Cage (C,n)))) and

 A3: p <> ( W-min ( L~ ( Cage (C,n))));



 A4: (LS /. 1) = Emax by JORDAN1F: 6;

 1 in ( dom LS) by FINSEQ_5: 6;

 then

 A5: (LS . 1) = Emax by A4, PARTFUN1:def 6;

 Ebo <> Wbo by SPRECT_1: 31;

 then p <> (LS . 1) by A2, A5, EUCLID: 52;

 then

 reconsider g1 = ( R_Cut (LS,p)) as being_S-Seq FinSequence of ( TOP-REAL 2) by A1, JORDAN3: 35;

 ( len g1) in ( dom g1) by FINSEQ_5: 6;



 then

 A6: (g1 /. ( len g1)) = (g1 . ( len g1)) by PARTFUN1:def 6

 .= p by A1, JORDAN3: 24;

 reconsider g = ( Rev g1) as being_S-Seq FinSequence of ( TOP-REAL 2);

 <*p*> is_in_the_area_of Ca by A1, JORDAN1E: 18, SPRECT_3: 46;

 then g1 is_in_the_area_of Ca by A1, JORDAN1E: 18, SPRECT_3: 52;

 then

 A7: g is_in_the_area_of Ca by SPRECT_3: 51;



 A8: (g /. 1) = (g1 /. ( len g1)) by FINSEQ_5: 65;



 A9: (g /. ( len g)) = (g /. ( len g1)) by FINSEQ_5:def 3

 .= (g1 /. 1) by FINSEQ_5: 65;

 ((g1 /. 1) `1 ) = ((LS /. 1) `1 ) by A1, SPRECT_3: 22

 .= (Emax `1 ) by JORDAN1F: 6

 .= Ebo by EUCLID: 52;

 then

 A10: g is_a_h.c._for Ca by A2, A7, A8, A9, A6, SPRECT_2:def 2;



 A11: (US /. 1) = Wmin by JORDAN1F: 5;

 1 in ( dom US) by FINSEQ_5: 6;

 then

 A12: (US . 1) = Wmin by A11, PARTFUN1:def 6;



 A13: ( L~ g) = ( L~ g1) by SPPOL_2: 22;

 ( len ( Cage (C,n))) > 4 by GOBOARD7: 34;

 then

 A14: ( rng ( Cage (C,n))) c= ( L~ ( Cage (C,n))) by SPPOL_2: 18, XXREAL_0: 2;

 now

 per cases ;

 suppose

 A15: Wmin <> SW;



 A16: not SW in ( rng ( Cage (C,n)))

 proof



 A17: (SW `1 ) = ( W-bound ( L~ ( Cage (C,n)))) by EUCLID: 52;



 A18: (SW `2 ) = ( S-bound ( L~ ( Cage (C,n)))) by EUCLID: 52;

 then (SW `2 ) <= ( N-bound ( L~ ( Cage (C,n)))) by SPRECT_1: 22;

 then SW in { p1 where p1 be Point of ( TOP-REAL 2) : (p1 `1 ) = ( W-bound ( L~ ( Cage (C,n)))) & (p1 `2 ) <= ( N-bound ( L~ ( Cage (C,n)))) & (p1 `2 ) >= ( S-bound ( L~ ( Cage (C,n)))) } by A17, A18;

 then

 A19: SW in ( LSeg (( SW-corner ( L~ ( Cage (C,n)))),( NW-corner ( L~ ( Cage (C,n)))))) by SPRECT_1: 26;

 assume SW in ( rng ( Cage (C,n)));

 then SW in (( LSeg (( SW-corner ( L~ ( Cage (C,n)))),( NW-corner ( L~ ( Cage (C,n)))))) /\ ( L~ ( Cage (C,n)))) by A14, A19, XBOOLE_0:def 4;

 then

 A20: (SW `2 ) >= (( W-min ( L~ ( Cage (C,n)))) `2 ) by PSCOMP_1: 31;



 A21: (( W-min ( L~ ( Cage (C,n)))) `1 ) = (SW `1 ) by PSCOMP_1: 29;

 (( W-min ( L~ ( Cage (C,n)))) `2 ) >= (SW `2 ) by PSCOMP_1: 30;

 then (( W-min ( L~ ( Cage (C,n)))) `2 ) = (SW `2 ) by A20, XXREAL_0: 1;

 hence contradiction by A15, A21, TOPREAL3: 6;

 end;

 Nmin in ( rng US) by Th7;

 then ( R_Cut (US,Nmin)) = ( mid (US,1,(Nmin .. US))) by JORDAN1G: 49;

 then

 A22: ( rng ( R_Cut (US,Nmin))) c= ( rng US) by FINSEQ_6: 119;

 ( rng US) c= ( rng Ca) by JORDAN1G: 39;

 then ( rng ( R_Cut (US,Nmin))) c= ( rng Ca) by A22;

 then not SW in ( rng ( R_Cut (US,Nmin))) by A16;

 then ( rng ( R_Cut (US,Nmin))) misses {SW} by ZFMISC_1: 50;

 then ( rng ( R_Cut (US,Nmin))) misses ( rng <*SW*>) by FINSEQ_1: 38;

 then

 A23: ( rng ( Rev ( R_Cut (US,Nmin)))) misses ( rng <*SW*>) by FINSEQ_5: 57;

 set h1 = (( Rev ( R_Cut (US,Nmin))) ^ <*SW*>);



 A24: <*SW*> is one-to-one by FINSEQ_3: 93;

 Wmax in ( L~ Ca) by SPRECT_1: 13;

 then

 A25: Nbo >= (Wmax `2 ) by PSCOMP_1: 24;



 A26: Nmin in ( L~ US) by Th7;

 then <*Nmin*> is_in_the_area_of Ca by JORDAN1E: 17, SPRECT_3: 46;

 then ( R_Cut (US,Nmin)) is_in_the_area_of Ca by A26, JORDAN1E: 17, SPRECT_3: 52;

 then

 A27: ( Rev ( R_Cut (US,Nmin))) is_in_the_area_of Ca by SPRECT_3: 51;

 (Wmax `2 ) > (Wmin `2 ) by SPRECT_2: 57;

 then

 A28: Nmin <> (US . 1) by A12, A25, EUCLID: 52;

 then

 reconsider RCutUS = ( R_Cut (US,Nmin)) as being_S-Seq FinSequence of ( TOP-REAL 2) by A26, JORDAN3: 35;



 A29: (( Rev RCutUS) /. ( len ( Rev RCutUS))) = (( Rev RCutUS) /. ( len RCutUS)) by FINSEQ_5:def 3

 .= (RCutUS /. 1) by FINSEQ_5: 65

 .= (US /. 1) by A26, SPRECT_3: 22

 .= Wmin by JORDAN1F: 5;



 then ((( Rev RCutUS) /. ( len ( Rev RCutUS))) `1 ) = ( W-bound ( L~ Ca)) by EUCLID: 52

 .= (SW `1 ) by EUCLID: 52

 .= (( <*SW*> /. 1) `1 ) by FINSEQ_4: 16;

 then

 reconsider h1 as one-to-one special FinSequence of ( TOP-REAL 2) by A23, A24, FINSEQ_3: 91, GOBOARD2: 8;

 set h = ( Rev h1);



 A30: h is special by SPPOL_2: 40;

 <*SW*> is_in_the_area_of Ca by SPRECT_2: 28;

 then h1 is_in_the_area_of Ca by A27, SPRECT_2: 24;

 then

 A31: h is_in_the_area_of Ca by SPRECT_3: 51;

 ( L~ h) = ( L~ h1) by SPPOL_2: 22;

 then

 A32: ( L~ h) = (( L~ ( Rev RCutUS)) \/ ( LSeg ((( Rev RCutUS) /. ( len ( Rev RCutUS))),SW))) by SPPOL_2: 19;



 A33: (( Index (Nmin,US)) + 1) >= ( 0 + 1) by XREAL_1: 7;



 A34: 2 <= ( len g) by TOPREAL1:def 8;

 ( len h1) = (( len ( Rev ( R_Cut (US,Nmin)))) + 1) by FINSEQ_2: 16

 .= (( len ( R_Cut (US,Nmin))) + 1) by FINSEQ_5:def 3

 .= ((( Index (Nmin,US)) + 1) + 1) by A26, A28, JORDAN3: 25;

 then ( len h1) >= (1 + 1) by A33, XREAL_1: 7;

 then

 A35: ( len h) >= 2 by FINSEQ_5:def 3;



 A36: (h /. 1) = (h1 /. ( len h1)) by FINSEQ_5: 65;



 A37: ( len US) in ( dom US) by FINSEQ_5: 6;

 1 in ( dom ( Rev RCutUS)) by FINSEQ_5: 6;



 then (h1 /. 1) = (( Rev RCutUS) /. 1) by FINSEQ_4: 68

 .= (( R_Cut (US,Nmin)) /. ( len ( R_Cut (US,Nmin)))) by FINSEQ_5: 65

 .= Nmin by A26, Th45;

 then

 A38: ((h1 /. 1) `2 ) = Nbo by EUCLID: 52;



 A39: ((h1 /. ( len h1)) `2 ) = ((h1 /. (( len ( Rev ( R_Cut (US,Nmin)))) + 1)) `2 ) by FINSEQ_2: 16

 .= (SW `2 ) by FINSEQ_4: 67

 .= Sbo by EUCLID: 52;



 A40: ( len LS) in ( dom LS) by FINSEQ_5: 6;

 (h /. ( len h)) = (h /. ( len h1)) by FINSEQ_5:def 3

 .= (h1 /. 1) by FINSEQ_5: 65;

 then h is_a_v.c._for Ca by A31, A38, A36, A39, SPRECT_2:def 3;

 then ( L~ g) meets ( L~ h) by A10, A30, A34, A35, SPRECT_2: 29;

 then

 consider x be object such that

 A41: x in ( L~ g) and

 A42: x in ( L~ h) by XBOOLE_0: 3;

 reconsider x as Point of ( TOP-REAL 2) by A41;



 A43: ( L~ RCutUS) c= ( L~ US) by Th7, JORDAN3: 41;



 A44: ( L~ g) c= ( L~ LS) by A1, A13, JORDAN3: 41;

 then

 A45: x in ( L~ LS) by A41;

 now

 per cases by A42, A32, XBOOLE_0:def 3;

 suppose x in ( L~ ( Rev RCutUS));

 then

 A46: x in ( L~ RCutUS) by SPPOL_2: 22;

 then x in (( L~ LS) /\ ( L~ US)) by A41, A44, A43, XBOOLE_0:def 4;

 then

 A47: x in {Emax, Wmin} by JORDAN1E: 16;

 now

 per cases by A47, TARSKI:def 2;

 suppose x = Emax;

 then (US /. ( len US)) in ( L~ ( R_Cut (US,Nmin))) by A46, JORDAN1F: 7;

 then (US . ( len US)) in ( L~ ( R_Cut (US,Nmin))) by A37, PARTFUN1:def 6;

 then (US . ( len US)) = Nmin by A26, Th43;

 then (US /. ( len US)) = Nmin by A37, PARTFUN1:def 6;

 then

 A48: Emax = Nmin by JORDAN1F: 7;

 Nmax in ( L~ Ca) by SPRECT_1: 11;

 then

 A49: Ebo >= (Nmax `1 ) by PSCOMP_1: 24;

 (Nmax `1 ) > (Nmin `1 ) by SPRECT_2: 51;

 hence contradiction by A48, A49, EUCLID: 52;

 end;

 suppose x = Wmin;

 then (LS /. ( len LS)) in ( L~ ( R_Cut (LS,p))) by A13, A41, JORDAN1F: 8;

 then (LS . ( len LS)) in ( L~ ( R_Cut (LS,p))) by A40, PARTFUN1:def 6;

 then (LS . ( len LS)) = p by A1, Th43;

 then (LS /. ( len LS)) = p by A40, PARTFUN1:def 6;

 hence contradiction by A3, JORDAN1F: 8;

 end;

 end;

 hence contradiction;

 end;

 suppose

 A50: x in ( LSeg ((( Rev RCutUS) /. ( len ( Rev RCutUS))),SW));

 (Wmin `2 ) >= (SW `2 ) by PSCOMP_1: 30;

 then

 A51: (Wmin `2 ) >= (x `2 ) by A29, A50, TOPREAL1: 4;



 A52: (Wmin `1 ) = Wbo by EUCLID: 52;

 (SW `1 ) = Wbo by EUCLID: 52;

 then

 A53: (x `1 ) = Wbo by A29, A50, A52, GOBOARD7: 5;

 ( L~ Ca) = (( L~ LS) \/ ( L~ US)) by JORDAN1E: 13;

 then ( L~ LS) c= ( L~ Ca) by XBOOLE_1: 7;

 then x in ( W-most ( L~ Ca)) by A45, A53, SPRECT_2: 12;

 then (x `2 ) >= (Wmin `2 ) by PSCOMP_1: 31;

 then (x `2 ) = (Wmin `2 ) by A51, XXREAL_0: 1;

 then x = Wmin by A52, A53, TOPREAL3: 6;

 then (LS /. ( len LS)) in ( L~ ( R_Cut (LS,p))) by A13, A41, JORDAN1F: 8;

 then (LS . ( len LS)) in ( L~ ( R_Cut (LS,p))) by A40, PARTFUN1:def 6;

 then (LS . ( len LS)) = p by A1, Th43;

 then (LS /. ( len LS)) = p by A40, PARTFUN1:def 6;

 hence contradiction by A3, JORDAN1F: 8;

 end;

 end;

 hence contradiction;

 end;

 suppose

 A54: Wmin = SW;

 set h = ( R_Cut (US,Nmin));



 A55: 2 <= ( len g) by TOPREAL1:def 8;

 Wmax in ( L~ Ca) by SPRECT_1: 13;

 then

 A56: Nbo >= (Wmax `2 ) by PSCOMP_1: 24;



 A57: Nmin in ( L~ US) by Th7;

 then <*Nmin*> is_in_the_area_of Ca by JORDAN1E: 17, SPRECT_3: 46;

 then

 A58: ( R_Cut (US,Nmin)) is_in_the_area_of Ca by A57, JORDAN1E: 17, SPRECT_3: 52;

 (Wmax `2 ) > (Wmin `2 ) by SPRECT_2: 57;

 then Nmin <> (US . 1) by A12, A56, EUCLID: 52;

 then

 reconsider RCutUS = ( R_Cut (US,Nmin)) as being_S-Seq FinSequence of ( TOP-REAL 2) by A57, JORDAN3: 35;



 A59: ( len RCutUS) >= 2 by TOPREAL1:def 8;

 (( R_Cut (US,Nmin)) /. ( len ( R_Cut (US,Nmin)))) = Nmin by A57, Th45;

 then

 A60: ((h /. ( len h)) `2 ) = Nbo by EUCLID: 52;

 (RCutUS /. 1) = (US /. 1) by A57, SPRECT_3: 22

 .= Wmin by JORDAN1F: 5;

 then ((h /. 1) `2 ) = Sbo by A54, EUCLID: 52;

 then h is_a_v.c._for Ca by A58, A60, SPRECT_2:def 3;

 then ( L~ g) meets ( L~ h) by A10, A55, A59, SPRECT_2: 29;

 then

 consider x be object such that

 A61: x in ( L~ g) and

 A62: x in ( L~ h) by XBOOLE_0: 3;

 reconsider x as Point of ( TOP-REAL 2) by A61;



 A63: ( len LS) in ( dom LS) by FINSEQ_5: 6;



 A64: ( L~ g) c= ( L~ LS) by A1, A13, JORDAN3: 41;



 A65: ( len US) in ( dom US) by FINSEQ_5: 6;

 ( L~ RCutUS) c= ( L~ US) by Th7, JORDAN3: 41;

 then x in (( L~ LS) /\ ( L~ US)) by A61, A62, A64, XBOOLE_0:def 4;

 then

 A66: x in {Emax, Wmin} by JORDAN1E: 16;

 now

 per cases by A66, TARSKI:def 2;

 suppose x = Emax;

 then (US /. ( len US)) in ( L~ ( R_Cut (US,Nmin))) by A62, JORDAN1F: 7;

 then (US . ( len US)) in ( L~ ( R_Cut (US,Nmin))) by A65, PARTFUN1:def 6;

 then (US . ( len US)) = Nmin by A57, Th43;

 then (US /. ( len US)) = Nmin by A65, PARTFUN1:def 6;

 then

 A67: Emax = Nmin by JORDAN1F: 7;

 Nmax in ( L~ Ca) by SPRECT_1: 11;

 then

 A68: Ebo >= (Nmax `1 ) by PSCOMP_1: 24;

 (Nmax `1 ) > (Nmin `1 ) by SPRECT_2: 51;

 hence contradiction by A67, A68, EUCLID: 52;

 end;

 suppose x = Wmin;

 then (LS /. ( len LS)) in ( L~ ( R_Cut (LS,p))) by A13, A61, JORDAN1F: 8;

 then (LS . ( len LS)) in ( L~ ( R_Cut (LS,p))) by A63, PARTFUN1:def 6;

 then (LS . ( len LS)) = p by A1, Th43;

 then (LS /. ( len LS)) = p by A63, PARTFUN1:def 6;

 hence contradiction by A3, JORDAN1F: 8;

 end;

 end;

 hence contradiction;

 end;

 end;

 hence contradiction;

 end;

 theorem :: JORDAN1J:48

 for G be Go-board holds for f,g be FinSequence of ( TOP-REAL 2) holds for k be Nat holds 1 <= k & k < ( len f) & (f ^ g) is_sequence_on G implies ( left_cell ((f ^ g),k,G)) = ( left_cell (f,k,G)) & ( right_cell ((f ^ g),k,G)) = ( right_cell (f,k,G))

 proof

 let G be Go-board;

 let f,g be FinSequence of ( TOP-REAL 2);

 let k be Nat;

 assume that

 A1: 1 <= k and

 A2: k < ( len f) and

 A3: (f ^ g) is_sequence_on G;



 A4: (k + 1) <= ( len f) by A2, NAT_1: 13;



 A5: ((f ^ g) | ( len f)) = f by FINSEQ_5: 23;

 ( len f) <= (( len f) + ( len g)) by NAT_1: 11;

 then ( len f) <= ( len (f ^ g)) by FINSEQ_1: 22;

 then (k + 1) <= ( len (f ^ g)) by A4, XXREAL_0: 2;

 hence thesis by A1, A3, A5, A4, GOBRD13: 31;

 end;

 theorem :: JORDAN1J:49



 Th49: for D be set holds for f,g be FinSequence of D holds for i be Nat st i <= ( len f) holds ((f ^' g) | i) = (f | i)

 proof

 let D be set;

 let f,g be FinSequence of D;

 let i be Nat;

 assume

 A1: i <= ( len f);

 then

 A2: ( len (f | i)) = i by FINSEQ_1: 59;

 per cases ;

 suppose

 A3: g <> {} ;

 then ( len g) >= ( 0 + 1) by NAT_1: 13;

 then (i + 1) <= (( len f) + ( len g)) by A1, XREAL_1: 7;

 then (i + 1) <= (( len (f ^' g)) + 1) by A3, FINSEQ_6: 139;

 then i <= ( len (f ^' g)) by XREAL_1: 6;

 then

 A4: ( len ((f ^' g) | i)) = i by FINSEQ_1: 59;

 then

 A5: ( dom ((f ^' g) | i)) = ( Seg i) by FINSEQ_1:def 3;

 now

 let j be Nat;

 assume

 A6: j in ( dom ((f ^' g) | i));

 then

 A7: 1 <= j by A5, FINSEQ_1: 1;

 j <= i by A5, A6, FINSEQ_1: 1;

 then

 A8: j <= ( len f) by A1, XXREAL_0: 2;



 thus (((f ^' g) | i) . j) = (((f ^' g) | ( Seg i)) . j) by FINSEQ_1:def 15

 .= ((f ^' g) . j) by A5, A6, FUNCT_1: 49

 .= (f . j) by A7, A8, FINSEQ_6: 140

 .= ((f | ( Seg i)) . j) by A5, A6, FUNCT_1: 49

 .= ((f | i) . j) by FINSEQ_1:def 15;

 end;

 hence thesis by A2, A4, FINSEQ_2: 9;

 end;

 suppose g = {} ;

 hence thesis by FINSEQ_6: 157;

 end;

 end;

 theorem :: JORDAN1J:50



 Th50: for D be set holds for f,g be FinSequence of D holds ((f ^' g) | ( len f)) = f

 proof

 let D be set;

 let f,g be FinSequence of D;

 (f | ( len f)) = (f | ( Seg ( len f))) by FINSEQ_1:def 15;

 hence thesis by Th49, FINSEQ_2: 20;

 end;

 theorem :: JORDAN1J:51



 Th51: for G be Go-board holds for f,g be FinSequence of ( TOP-REAL 2) holds for k be Nat holds 1 <= k & k < ( len f) & (f ^' g) is_sequence_on G implies ( left_cell ((f ^' g),k,G)) = ( left_cell (f,k,G)) & ( right_cell ((f ^' g),k,G)) = ( right_cell (f,k,G))

 proof

 let G be Go-board;

 let f,g be FinSequence of ( TOP-REAL 2);

 let k be Nat;

 assume that

 A1: 1 <= k and

 A2: k < ( len f) and

 A3: (f ^' g) is_sequence_on G;



 A4: (k + 1) <= ( len f) by A2, NAT_1: 13;



 A5: ((f ^' g) | ( len f)) = f by Th50;

 ( len f) <= ( len (f ^' g)) by TOPREAL8: 7;

 then (k + 1) <= ( len (f ^' g)) by A4, XXREAL_0: 2;

 hence thesis by A1, A3, A5, A4, GOBRD13: 31;

 end;

 theorem :: JORDAN1J:52



 Th52: for G be Go-board holds for f be S-Sequence_in_R2 holds for p be Point of ( TOP-REAL 2) holds for k be Nat st 1 <= k & k < (p .. f) & f is_sequence_on G & p in ( rng f) holds ( left_cell (( R_Cut (f,p)),k,G)) = ( left_cell (f,k,G)) & ( right_cell (( R_Cut (f,p)),k,G)) = ( right_cell (f,k,G))

 proof

 let G be Go-board;

 let f be S-Sequence_in_R2;

 let p be Point of ( TOP-REAL 2);

 let k be Nat;

 assume that

 A1: 1 <= k and

 A2: k < (p .. f) and

 A3: f is_sequence_on G and

 A4: p in ( rng f);



 A5: (f | (p .. f)) = ( mid (f,1,(p .. f))) by A1, A2, FINSEQ_6: 116, XXREAL_0: 2

 .= ( R_Cut (f,p)) by A4, JORDAN1G: 49;



 A6: (k + 1) <= (p .. f) by A2, NAT_1: 13;

 (p .. f) <= ( len f) by A4, FINSEQ_4: 21;

 then (k + 1) <= ( len f) by A6, XXREAL_0: 2;

 hence thesis by A1, A3, A5, A6, GOBRD13: 31;

 end;

 theorem :: JORDAN1J:53



 Th53: for G be Go-board holds for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) holds for k be Nat st 1 <= k & k < (p .. f) & f is_sequence_on G holds ( left_cell ((f -: p),k,G)) = ( left_cell (f,k,G)) & ( right_cell ((f -: p),k,G)) = ( right_cell (f,k,G))

 proof

 let G be Go-board;

 let f be FinSequence of ( TOP-REAL 2);

 let p be Point of ( TOP-REAL 2);

 let k be Nat;

 assume that

 A1: 1 <= k and

 A2: k < (p .. f) and

 A3: f is_sequence_on G;



 A4: (k + 1) <= (p .. f) by A2, NAT_1: 13;



 A5: (f | (p .. f)) = (f -: p) by FINSEQ_5:def 1;

 per cases by TOPREAL8: 4;

 suppose p in ( rng f);

 then (p .. f) <= ( len f) by FINSEQ_4: 21;

 then (k + 1) <= ( len f) by A4, XXREAL_0: 2;

 hence thesis by A1, A3, A5, A4, GOBRD13: 31;

 end;

 suppose (p .. f) = 0 ;

 hence thesis by A2;

 end;

 end;

 theorem :: JORDAN1J:54



 Th54: for f,g be FinSequence of ( TOP-REAL 2) st f is unfolded s.n.c. one-to-one & g is unfolded s.n.c. one-to-one & (f /. ( len f)) = (g /. 1) & (( L~ f) /\ ( L~ g)) = {(g /. 1)} holds (f ^' g) is s.n.c.

 proof

 let f,g be FinSequence of ( TOP-REAL 2);

 assume that

 A1: f is unfolded s.n.c. one-to-one and

 A2: g is unfolded s.n.c. one-to-one and

 A3: (f /. ( len f)) = (g /. 1) and

 A4: (( L~ f) /\ ( L~ g)) = {(g /. 1)};

 now

 let i,j be Nat;

 assume

 A5: (i + 1) < j;

 now

 per cases ;

 suppose

 A6: j < ( len f);

 then (i + 1) < ( len f) by A5, XXREAL_0: 2;

 then i < ( len f) by NAT_1: 13;

 then

 A7: ( LSeg ((f ^' g),i)) = ( LSeg (f,i)) by TOPREAL8: 28;

 ( LSeg ((f ^' g),j)) = ( LSeg (f,j)) by A6, TOPREAL8: 28;

 hence ( LSeg ((f ^' g),i)) misses ( LSeg ((f ^' g),j)) by A1, A5, A7, TOPREAL1:def 7;

 end;

 suppose j >= ( len f);

 then

 consider k be Nat such that

 A8: j = (( len f) + k) by NAT_1: 10;

 A9:

 now

 assume g is trivial;

 then ( len g) < 2 by NAT_D: 60;

 then ( len g) = 0 or ( len g) = 1 by NAT_1: 23;

 then ( L~ g) = {} by TOPREAL1: 22;

 hence contradiction by A4;

 end;

 reconsider k as Nat;

 A10:

 now

 assume f is empty;

 then ( len f) = 0 ;

 then ( L~ f) = {} by TOPREAL1: 22;

 hence contradiction by A4;

 end;

 now

 per cases ;

 suppose

 A11: i >= 1 & (j + 1) <= ( len (f ^' g));

 then (j + 1) < (( len (f ^' g)) + 1) by NAT_1: 13;

 then (( len f) + (k + 1)) < (( len f) + ( len g)) by A8, A9, FINSEQ_6: 139;

 then

 A12: (k + 1) < ( len g) by XREAL_1: 7;

 then

 A13: ( LSeg ((f ^' g),(( len f) + k))) = ( LSeg (g,(k + 1))) by A3, A10, A9, TOPREAL8: 31;

 then

 A14: ( LSeg ((f ^' g),j)) c= ( L~ g) by A8, TOPREAL3: 19;

 now

 per cases ;

 suppose

 A15: i < ( len f);

 then

 A16: (i + 1) <= ( len f) by NAT_1: 13;

 (i + 1) > 1 by A11, NAT_1: 13;

 then

 A17: (i + 1) in ( dom f) by A16, FINSEQ_3: 25;



 A18: ( len g) >= 2 by A9, NAT_D: 60;



 A19: ( LSeg ((f ^' g),i)) = ( LSeg (f,i)) by A15, TOPREAL8: 28;

 then ( LSeg ((f ^' g),i)) c= ( L~ f) by TOPREAL3: 19;

 then

 A20: (( LSeg ((f ^' g),i)) /\ ( LSeg ((f ^' g),j))) c= {(g /. 1)} by A4, A14, XBOOLE_1: 27;

 assume ( LSeg ((f ^' g),i)) meets ( LSeg ((f ^' g),j));

 then

 consider x be object such that

 A21: x in ( LSeg ((f ^' g),i)) and

 A22: x in ( LSeg ((f ^' g),j)) by XBOOLE_0: 3;

 x in (( LSeg ((f ^' g),i)) /\ ( LSeg ((f ^' g),j))) by A21, A22, XBOOLE_0:def 4;

 then

 A23: x = (g /. 1) by A20, TARSKI:def 1;

 i in ( dom f) by A11, A15, FINSEQ_3: 25;

 then (( len f) + 0 ) < (( len f) + k) by A1, A3, A5, A8, A19, A21, A23, A17, GOBOARD2: 2;

 then k > 0 ;

 then (k + 1) > ( 0 + 1) by XREAL_1: 6;

 hence contradiction by A2, A8, A13, A22, A23, A18, JORDAN5B: 30;

 end;

 suppose i >= ( len f);

 then

 consider l be Nat such that

 A24: i = (( len f) + l) by NAT_1: 10;

 reconsider l as Nat;

 (( len f) + (l + 1)) < (( len f) + k) by A5, A8, A24;

 then (l + 1) < k by XREAL_1: 7;

 then

 A25: ((l + 1) + 1) < (k + 1) by XREAL_1: 6;

 then ((l + 1) + 1) < ( len g) by A12, XXREAL_0: 2;

 then (l + 1) < ( len g) by NAT_1: 13;

 then ( LSeg ((f ^' g),(( len f) + l))) = ( LSeg (g,(l + 1))) by A3, A10, A9, TOPREAL8: 31;

 hence ( LSeg ((f ^' g),i)) misses ( LSeg ((f ^' g),j)) by A2, A8, A13, A24, A25, TOPREAL1:def 7;

 end;

 end;

 hence ( LSeg ((f ^' g),i)) misses ( LSeg ((f ^' g),j));

 end;

 suppose (j + 1) > ( len (f ^' g));

 then ( LSeg ((f ^' g),j)) = {} by TOPREAL1:def 3;

 hence ( LSeg ((f ^' g),i)) misses ( LSeg ((f ^' g),j));

 end;

 suppose i < 1;

 then ( LSeg ((f ^' g),i)) = {} by TOPREAL1:def 3;

 hence ( LSeg ((f ^' g),i)) misses ( LSeg ((f ^' g),j));

 end;

 end;

 hence ( LSeg ((f ^' g),i)) misses ( LSeg ((f ^' g),j));

 end;

 end;

 hence ( LSeg ((f ^' g),i)) misses ( LSeg ((f ^' g),j));

 end;

 hence thesis by TOPREAL1:def 7;

 end;

 theorem :: JORDAN1J:55



 Th55: for f,g be FinSequence of ( TOP-REAL 2) st f is one-to-one & g is one-to-one & (( rng f) /\ ( rng g)) c= {(g /. 1)} holds (f ^' g) is one-to-one

 proof

 let f,g be FinSequence of ( TOP-REAL 2);

 assume that

 A1: f is one-to-one and

 A2: g is one-to-one and

 A3: (( rng f) /\ ( rng g)) c= {(g /. 1)};

 per cases ;

 suppose

 A4: ( rng g) <> {} ;

 now



 A5: (( len (f ^' g)) + 1) = (( len f) + ( len g)) by A4, FINSEQ_6: 139, RELAT_1: 38;

 let i,j be Element of NAT ;

 assume that

 A6: i in ( dom (f ^' g)) and

 A7: j in ( dom (f ^' g)) and

 A8: ((f ^' g) /. i) = ((f ^' g) /. j);



 A9: 1 <= i by A6, FINSEQ_3: 25;

 j <= ( len (f ^' g)) by A7, FINSEQ_3: 25;

 then

 A10: j < (( len f) + ( len g)) by A5, NAT_1: 13;



 A11: ( len f) = (( len f) + 0 );

 i <= ( len (f ^' g)) by A6, FINSEQ_3: 25;

 then

 A12: i < (( len f) + ( len g)) by A5, NAT_1: 13;



 A13: 1 <= j by A7, FINSEQ_3: 25;



 A14: 1 in ( dom g) by A4, FINSEQ_3: 32;

 now

 per cases ;

 suppose

 A15: i <= ( len f) & j <= ( len f);

 then

 A16: i in ( dom f) by A9, FINSEQ_3: 25;



 A17: ((f ^' g) /. j) = (f /. j) by A13, A15, FINSEQ_6: 159;



 A18: j in ( dom f) by A13, A15, FINSEQ_3: 25;

 ((f ^' g) /. i) = (f /. i) by A9, A15, FINSEQ_6: 159;

 hence i = j by A1, A8, A17, A16, A18, PARTFUN2: 10;

 end;

 suppose

 A19: i > ( len f) & j > ( len f);

 then

 consider l be Nat such that

 A20: j = (( len f) + l) by NAT_1: 10;

 consider k be Nat such that

 A21: i = (( len f) + k) by A19, NAT_1: 10;

 reconsider k, l as Element of NAT by ORDINAL1:def 12;

 l > 0 by A11, A19, A20;

 then

 A22: l >= ( 0 + 1) by NAT_1: 13;

 then

 A23: (l + 1) > 1 by NAT_1: 13;

 k > 0 by A11, A19, A21;

 then

 A24: k >= ( 0 + 1) by NAT_1: 13;

 then

 A25: (k + 1) > 1 by NAT_1: 13;



 A26: l < ( len g) by A10, A20, XREAL_1: 7;

 then

 A27: ((f ^' g) /. j) = (g /. (l + 1)) by A20, A22, FINSEQ_6: 160;



 A28: k < ( len g) by A12, A21, XREAL_1: 7;

 then (k + 1) <= ( len g) by NAT_1: 13;

 then

 A29: (k + 1) in ( dom g) by A25, FINSEQ_3: 25;

 (l + 1) <= ( len g) by A26, NAT_1: 13;

 then

 A30: (l + 1) in ( dom g) by A23, FINSEQ_3: 25;

 ((f ^' g) /. i) = (g /. (k + 1)) by A21, A28, A24, FINSEQ_6: 160;

 then (k + 1) = (l + 1) by A2, A8, A27, A29, A30, PARTFUN2: 10;

 hence i = j by A21, A20;

 end;

 suppose

 A31: i <= ( len f) & j > ( len f);

 then

 A32: i in ( dom f) by A9, FINSEQ_3: 25;

 ((f ^' g) /. i) = (f /. i) by A9, A31, FINSEQ_6: 159;

 then

 A33: ((f ^' g) /. i) in ( rng f) by A32, PARTFUN2: 2;

 consider l be Nat such that

 A34: j = (( len f) + l) by A31, NAT_1: 10;

 reconsider l as Element of NAT by ORDINAL1:def 12;

 l > 0 by A11, A31, A34;

 then

 A35: l >= ( 0 + 1) by NAT_1: 13;

 then

 A36: (l + 1) > 1 by NAT_1: 13;



 A37: l < ( len g) by A10, A34, XREAL_1: 7;

 then (l + 1) <= ( len g) by NAT_1: 13;

 then

 A38: (l + 1) in ( dom g) by A36, FINSEQ_3: 25;



 A39: ((f ^' g) /. j) = (g /. (l + 1)) by A34, A37, A35, FINSEQ_6: 160;

 then ((f ^' g) /. j) in ( rng g) by A38, PARTFUN2: 2;

 then ((f ^' g) /. j) in (( rng f) /\ ( rng g)) by A8, A33, XBOOLE_0:def 4;

 then (g /. (l + 1)) = (g /. 1) by A3, A39, TARSKI:def 1;

 hence i = j by A2, A14, A36, A38, PARTFUN2: 10;

 end;

 suppose

 A40: j <= ( len f) & i > ( len f);

 then

 A41: j in ( dom f) by A13, FINSEQ_3: 25;

 ((f ^' g) /. j) = (f /. j) by A13, A40, FINSEQ_6: 159;

 then

 A42: ((f ^' g) /. j) in ( rng f) by A41, PARTFUN2: 2;

 consider l be Nat such that

 A43: i = (( len f) + l) by A40, NAT_1: 10;

 reconsider l as Element of NAT by ORDINAL1:def 12;

 l > 0 by A11, A40, A43;

 then

 A44: l >= ( 0 + 1) by NAT_1: 13;

 then

 A45: (l + 1) > 1 by NAT_1: 13;



 A46: l < ( len g) by A12, A43, XREAL_1: 7;

 then (l + 1) <= ( len g) by NAT_1: 13;

 then

 A47: (l + 1) in ( dom g) by A45, FINSEQ_3: 25;



 A48: ((f ^' g) /. i) = (g /. (l + 1)) by A43, A46, A44, FINSEQ_6: 160;

 then ((f ^' g) /. i) in ( rng g) by A47, PARTFUN2: 2;

 then ((f ^' g) /. i) in (( rng f) /\ ( rng g)) by A8, A42, XBOOLE_0:def 4;

 then (g /. (l + 1)) = (g /. 1) by A3, A48, TARSKI:def 1;

 hence i = j by A2, A14, A45, A47, PARTFUN2: 10;

 end;

 end;

 hence i = j;

 end;

 hence thesis by PARTFUN2: 9;

 end;

 suppose ( rng g) = {} ;

 then g = {} by RELAT_1: 41;

 hence thesis by A1, FINSEQ_6: 157;

 end;

 end;

 theorem :: JORDAN1J:56



 Th56: for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st f is being_S-Seq & p in ( rng f) & p <> (f . 1) holds (( Index (p,f)) + 1) = (p .. f)

 proof

 let f be FinSequence of ( TOP-REAL 2);

 let p be Point of ( TOP-REAL 2);

 assume that

 A1: f is being_S-Seq and

 A2: p in ( rng f) and

 A3: p <> (f . 1);



 A4: 1 <= (p .. f) by A2, FINSEQ_4: 21;

 (p .. f) <> 1 by A2, A3, FINSEQ_4: 19;

 then

 A5: 1 < (p .. f) by A4, XXREAL_0: 1;



 A6: (f . (p .. f)) = p by A2, FINSEQ_4: 19;

 (p .. f) <= ( len f) by A2, FINSEQ_4: 21;

 hence thesis by A1, A5, A6, JORDAN3: 12;

 end;

 theorem :: JORDAN1J:57



 Th57: for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds for i,j,k be Nat st 1 k

 proof

 let C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2);

 let i,j,k be Nat;

 assume that

 A1: 1 < i and

 A2: i < ( len ( Gauge (C,n))) and

 A3: 1 <= j and

 A4: k <= ( width ( Gauge (C,n))) and

 A5: (( Gauge (C,n)) * (i,k)) in ( L~ ( Upper_Seq (C,n))) and

 A6: (( Gauge (C,n)) * (i,j)) in ( L~ ( Lower_Seq (C,n))) and

 A7: j = k;



 A8: [i, j] in ( Indices ( Gauge (C,n))) by A1, A2, A3, A4, A7, MATRIX_0: 30;

 (( Gauge (C,n)) * (i,k)) in (( L~ ( Upper_Seq (C,n))) /\ ( L~ ( Lower_Seq (C,n)))) by A5, A6, A7, XBOOLE_0:def 4;

 then

 A9: (( Gauge (C,n)) * (i,k)) in {( W-min ( L~ ( Cage (C,n)))), ( E-max ( L~ ( Cage (C,n))))} by JORDAN1E: 16;



 A10: ( len ( Gauge (C,n))) = ( width ( Gauge (C,n))) by JORDAN8:def 1;

 ( len ( Gauge (C,n))) >= 4 by JORDAN8: 10;

 then

 A11: ( len ( Gauge (C,n))) >= 1 by XXREAL_0: 2;

 then

 A12: [( len ( Gauge (C,n))), j] in ( Indices ( Gauge (C,n))) by A3, A4, A7, MATRIX_0: 30;



 A13: [1, j] in ( Indices ( Gauge (C,n))) by A3, A4, A7, A11, MATRIX_0: 30;

 per cases by A9, TARSKI:def 2;

 suppose

 A14: (( Gauge (C,n)) * (i,k)) = ( W-min ( L~ ( Cage (C,n))));

 ((( Gauge (C,n)) * (1,j)) `1 ) = ( W-bound ( L~ ( Cage (C,n)))) by A3, A4, A7, A10, JORDAN1A: 73;

 then (( W-min ( L~ ( Cage (C,n)))) `1 ) <> ( W-bound ( L~ ( Cage (C,n)))) by A1, A7, A8, A13, A14, JORDAN1G: 7;

 hence contradiction by EUCLID: 52;

 end;

 suppose

 A15: (( Gauge (C,n)) * (i,k)) = ( E-max ( L~ ( Cage (C,n))));

 ((( Gauge (C,n)) * (( len ( Gauge (C,n))),j)) `1 ) = ( E-bound ( L~ ( Cage (C,n)))) by A3, A4, A7, A10, JORDAN1A: 71;

 then (( E-max ( L~ ( Cage (C,n)))) `1 ) <> ( E-bound ( L~ ( Cage (C,n)))) by A2, A7, A8, A12, A15, JORDAN1G: 7;

 hence contradiction by EUCLID: 52;

 end;

 end;

 theorem :: JORDAN1J:58



 Th58: for C be Simple_closed_curve holds for i,j,k be Nat st 1 < i & i < ( len ( Gauge (C,n))) & 1 <= j & j <= k & k <= ( width ( Gauge (C,n))) & (( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) /\ ( L~ ( Upper_Seq (C,n)))) = {(( Gauge (C,n)) * (i,k))} & (( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) /\ ( L~ ( Lower_Seq (C,n)))) = {(( Gauge (C,n)) * (i,j))} holds ( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) meets ( Lower_Arc C)

 proof

 let C be Simple_closed_curve;

 let i,j,k be Nat;

 set Ga = ( Gauge (C,n));

 set US = ( Upper_Seq (C,n));

 set LS = ( Lower_Seq (C,n));

 set LA = ( Lower_Arc C);

 set Wmin = ( W-min ( L~ ( Cage (C,n))));

 set Emax = ( E-max ( L~ ( Cage (C,n))));

 set Wbo = ( W-bound ( L~ ( Cage (C,n))));

 set Ebo = ( E-bound ( L~ ( Cage (C,n))));

 set Gij = (Ga * (i,j));

 set Gik = (Ga * (i,k));

 assume that

 A1: 1 < i and

 A2: i < ( len Ga) and

 A3: 1 <= j and

 A4: j <= k and

 A5: k <= ( width Ga) and

 A6: (( LSeg (Gij,Gik)) /\ ( L~ US)) = {Gik} and

 A7: (( LSeg (Gij,Gik)) /\ ( L~ LS)) = {Gij} and

 A8: ( LSeg (Gij,Gik)) misses LA;

 Gij in {Gij} by TARSKI:def 1;

 then

 A9: Gij in ( L~ LS) by A7, XBOOLE_0:def 4;

 Gik in {Gik} by TARSKI:def 1;

 then

 A10: Gik in ( L~ US) by A6, XBOOLE_0:def 4;

 then

 A11: j <> k by A1, A2, A3, A5, A9, Th57;



 A12: j <= ( width Ga) by A4, A5, XXREAL_0: 2;



 A13: 1 <= k by A3, A4, XXREAL_0: 2;



 A14: [i, j] in ( Indices Ga) by A1, A2, A3, A12, MATRIX_0: 30;



 A15: [i, k] in ( Indices Ga) by A1, A2, A5, A13, MATRIX_0: 30;

 set go = ( R_Cut (US,Gik));

 set co = ( L_Cut (LS,Gij));



 A16: ( len Ga) = ( width Ga) by JORDAN8:def 1;



 A17: ( len US) >= 3 by JORDAN1E: 15;

 then ( len US) >= 1 by XXREAL_0: 2;

 then 1 in ( dom US) by FINSEQ_3: 25;



 then

 A18: (US . 1) = (US /. 1) by PARTFUN1:def 6

 .= Wmin by JORDAN1F: 5;



 A19: (Wmin `1 ) = Wbo by EUCLID: 52

 .= ((Ga * (1,k)) `1 ) by A5, A13, A16, JORDAN1A: 73;

 ( len Ga) >= 4 by JORDAN8: 10;

 then

 A20: ( len Ga) >= 1 by XXREAL_0: 2;

 then

 A21: [1, k] in ( Indices Ga) by A5, A13, MATRIX_0: 30;

 then

 A22: Gik <> (US . 1) by A1, A15, A18, A19, JORDAN1G: 7;

 then

 reconsider go as being_S-Seq FinSequence of ( TOP-REAL 2) by A10, JORDAN3: 35;



 A23: ( len LS) >= (1 + 2) by JORDAN1E: 15;

 then

 A24: ( len LS) >= 1 by XXREAL_0: 2;

 then

 A25: 1 in ( dom LS) by FINSEQ_3: 25;

 ( len LS) in ( dom LS) by A24, FINSEQ_3: 25;



 then

 A26: (LS . ( len LS)) = (LS /. ( len LS)) by PARTFUN1:def 6

 .= Wmin by JORDAN1F: 8;



 A27: (Wmin `1 ) = Wbo by EUCLID: 52

 .= ((Ga * (1,k)) `1 ) by A5, A13, A16, JORDAN1A: 73;



 A28: [i, j] in ( Indices Ga) by A1, A2, A3, A12, MATRIX_0: 30;

 then

 A29: Gij <> (LS . ( len LS)) by A1, A21, A26, A27, JORDAN1G: 7;

 then

 reconsider co as being_S-Seq FinSequence of ( TOP-REAL 2) by A9, JORDAN3: 34;



 A30: [( len Ga), k] in ( Indices Ga) by A5, A13, A20, MATRIX_0: 30;



 A31: (LS . 1) = (LS /. 1) by A25, PARTFUN1:def 6

 .= Emax by JORDAN1F: 6;

 (Emax `1 ) = Ebo by EUCLID: 52

 .= ((Ga * (( len Ga),k)) `1 ) by A5, A13, A16, JORDAN1A: 71;

 then

 A32: Gij <> (LS . 1) by A2, A28, A30, A31, JORDAN1G: 7;



 A33: ( len go) >= (1 + 1) by TOPREAL1:def 8;



 A34: Gik in ( rng US) by A1, A2, A5, A10, A13, Th40, JORDAN1G: 4;

 then

 A35: go is_sequence_on Ga by Th38, JORDAN1G: 4;



 A36: ( len co) >= (1 + 1) by TOPREAL1:def 8;



 A37: Gij in ( rng LS) by A1, A2, A3, A9, A12, Th40, JORDAN1G: 5;

 then

 A38: co is_sequence_on Ga by Th39, JORDAN1G: 5;

 reconsider go as non constant s.c.c. being_S-Seq FinSequence of ( TOP-REAL 2) by A33, A35, JGRAPH_1: 12, JORDAN8: 5;

 reconsider co as non constant s.c.c. being_S-Seq FinSequence of ( TOP-REAL 2) by A36, A38, JGRAPH_1: 12, JORDAN8: 5;



 A39: ( len go) > 1 by A33, NAT_1: 13;

 then

 A40: ( len go) in ( dom go) by FINSEQ_3: 25;



 then

 A41: (go /. ( len go)) = (go . ( len go)) by PARTFUN1:def 6

 .= Gik by A10, JORDAN3: 24;

 ( len co) >= 1 by A36, XXREAL_0: 2;

 then 1 in ( dom co) by FINSEQ_3: 25;



 then

 A42: (co /. 1) = (co . 1) by PARTFUN1:def 6

 .= Gij by A9, JORDAN3: 23;

 reconsider m = (( len go) - 1) as Nat by A40, FINSEQ_3: 26;



 A43: (m + 1) = ( len go);

 then

 A44: (( len go) -' 1) = m by NAT_D: 34;



 A45: ( LSeg (go,m)) c= ( L~ go) by TOPREAL3: 19;



 A46: ( L~ go) c= ( L~ US) by A10, JORDAN3: 41;

 then ( LSeg (go,m)) c= ( L~ US) by A45;

 then

 A47: (( LSeg (go,m)) /\ ( LSeg (Gik,Gij))) c= {Gik} by A6, XBOOLE_1: 26;

 m >= 1 by A33, XREAL_1: 19;

 then

 A48: ( LSeg (go,m)) = ( LSeg ((go /. m),Gik)) by A41, A43, TOPREAL1:def 3;

 {Gik} c= (( LSeg (go,m)) /\ ( LSeg (Gik,Gij)))

 proof

 let x be object;



 A49: Gik in ( LSeg (Gik,Gij)) by RLTOPSP1: 68;

 assume x in {Gik};

 then

 A50: x = Gik by TARSKI:def 1;

 Gik in ( LSeg (go,m)) by A48, RLTOPSP1: 68;

 hence thesis by A50, A49, XBOOLE_0:def 4;

 end;

 then

 A51: (( LSeg (go,m)) /\ ( LSeg (Gik,Gij))) = {Gik} by A47;



 A52: ( LSeg (co,1)) c= ( L~ co) by TOPREAL3: 19;



 A53: ( L~ co) c= ( L~ LS) by A9, JORDAN3: 42;

 then ( LSeg (co,1)) c= ( L~ LS) by A52;

 then

 A54: (( LSeg (co,1)) /\ ( LSeg (Gik,Gij))) c= {Gij} by A7, XBOOLE_1: 26;



 A55: ( LSeg (co,1)) = ( LSeg (Gij,(co /. (1 + 1)))) by A36, A42, TOPREAL1:def 3;

 {Gij} c= (( LSeg (co,1)) /\ ( LSeg (Gik,Gij)))

 proof

 let x be object;



 A56: Gij in ( LSeg (Gik,Gij)) by RLTOPSP1: 68;

 assume x in {Gij};

 then

 A57: x = Gij by TARSKI:def 1;

 Gij in ( LSeg (co,1)) by A55, RLTOPSP1: 68;

 hence thesis by A57, A56, XBOOLE_0:def 4;

 end;

 then

 A58: (( LSeg (Gik,Gij)) /\ ( LSeg (co,1))) = {Gij} by A54;



 A59: (go /. 1) = (US /. 1) by A10, SPRECT_3: 22

 .= Wmin by JORDAN1F: 5;



 then

 A60: (go /. 1) = (LS /. ( len LS)) by JORDAN1F: 8

 .= (co /. ( len co)) by A9, Th35;



 A61: ( rng go) c= ( L~ go) by A33, SPPOL_2: 18;



 A62: ( rng co) c= ( L~ co) by A36, SPPOL_2: 18;



 A63: {(go /. 1)} c= (( L~ go) /\ ( L~ co))

 proof

 let x be object;

 assume x in {(go /. 1)};

 then

 A64: x = (go /. 1) by TARSKI:def 1;

 then

 A65: x in ( rng go) by FINSEQ_6: 42;

 x in ( rng co) by A60, A64, FINSEQ_6: 168;

 hence thesis by A61, A62, A65, XBOOLE_0:def 4;

 end;



 A66: (LS . 1) = (LS /. 1) by A25, PARTFUN1:def 6

 .= Emax by JORDAN1F: 6;



 A67: [( len Ga), j] in ( Indices Ga) by A3, A12, A20, MATRIX_0: 30;

 (( L~ go) /\ ( L~ co)) c= {(go /. 1)}

 proof

 let x be object;

 assume

 A68: x in (( L~ go) /\ ( L~ co));

 then

 A69: x in ( L~ co) by XBOOLE_0:def 4;

 A70:

 now

 assume x = Emax;

 then

 A71: Emax = Gij by A9, A66, A69, JORDAN1E: 7;

 ((Ga * (( len Ga),j)) `1 ) = Ebo by A3, A12, A16, JORDAN1A: 71;

 then (Emax `1 ) <> Ebo by A2, A14, A67, A71, JORDAN1G: 7;

 hence contradiction by EUCLID: 52;

 end;

 x in ( L~ go) by A68, XBOOLE_0:def 4;

 then x in (( L~ US) /\ ( L~ LS)) by A46, A53, A69, XBOOLE_0:def 4;

 then x in {Wmin, Emax} by JORDAN1E: 16;

 then x = Wmin or x = Emax by TARSKI:def 2;

 hence thesis by A59, A70, TARSKI:def 1;

 end;

 then

 A72: (( L~ go) /\ ( L~ co)) = {(go /. 1)} by A63;

 set W2 = (go /. 2);



 A73: 2 in ( dom go) by A33, FINSEQ_3: 25;

 A74:

 now

 assume (Gik `1 ) = Wbo;

 then ((Ga * (1,k)) `1 ) = ((Ga * (i,k)) `1 ) by A5, A13, A16, JORDAN1A: 73;

 hence contradiction by A1, A15, A21, JORDAN1G: 7;

 end;

 go = ( mid (US,1,(Gik .. US))) by A34, JORDAN1G: 49

 .= (US | (Gik .. US)) by A34, FINSEQ_4: 21, FINSEQ_6: 116;

 then

 A75: W2 = (US /. 2) by A73, FINSEQ_4: 70;

 set pion = <*Gik, Gij*>;

 A76:

 now

 let n be Nat;

 assume n in ( dom pion);

 then n in ( Seg 2) by FINSEQ_1: 89;

 then n = 1 or n = 2 by FINSEQ_1: 2, TARSKI:def 2;

 hence ex i,j be Nat st [i, j] in ( Indices Ga) & (pion /. n) = (Ga * (i,j)) by A14, A15, FINSEQ_4: 17;

 end;



 A77: Gik <> Gij by A11, A14, A15, GOBOARD1: 5;



 A78: (Gik `1 ) = ((Ga * (i,1)) `1 ) by A1, A2, A5, A13, GOBOARD5: 2

 .= (Gij `1 ) by A1, A2, A3, A12, GOBOARD5: 2;

 then ( LSeg (Gik,Gij)) is vertical by SPPOL_1: 16;

 then pion is being_S-Seq by A77, JORDAN1B: 7;

 then

 consider pion1 be FinSequence of ( TOP-REAL 2) such that

 A79: pion1 is_sequence_on Ga and

 A80: pion1 is being_S-Seq and

 A81: ( L~ pion) = ( L~ pion1) and

 A82: (pion /. 1) = (pion1 /. 1) and

 A83: (pion /. ( len pion)) = (pion1 /. ( len pion1)) and

 A84: ( len pion) <= ( len pion1) by A76, GOBOARD3: 2;

 reconsider pion1 as being_S-Seq FinSequence of ( TOP-REAL 2) by A80;

 set godo = ((go ^' pion1) ^' co);



 A85: (1 + 1) <= ( len ( Cage (C,n))) by GOBOARD7: 34, XXREAL_0: 2;



 A86: (1 + 1) <= ( len ( Rotate (( Cage (C,n)),Wmin))) by GOBOARD7: 34, XXREAL_0: 2;

 ( len (go ^' pion1)) >= ( len go) by TOPREAL8: 7;

 then

 A87: ( len (go ^' pion1)) >= (1 + 1) by A33, XXREAL_0: 2;

 then

 A88: ( len (go ^' pion1)) > (1 + 0 ) by NAT_1: 13;



 A89: ( len godo) >= ( len (go ^' pion1)) by TOPREAL8: 7;

 then

 A90: (1 + 1) <= ( len godo) by A87, XXREAL_0: 2;



 A91: US is_sequence_on Ga by JORDAN1G: 4;



 A92: (go /. ( len go)) = (pion1 /. 1) by A41, A82, FINSEQ_4: 17;

 then

 A93: (go ^' pion1) is_sequence_on Ga by A35, A79, TOPREAL8: 12;



 A94: ((go ^' pion1) /. ( len (go ^' pion1))) = (pion /. ( len pion)) by A83, FINSEQ_6: 156

 .= (pion /. 2) by FINSEQ_1: 44

 .= (co /. 1) by A42, FINSEQ_4: 17;

 then

 A95: godo is_sequence_on Ga by A38, A93, TOPREAL8: 12;

 ( LSeg (pion1,1)) c= ( L~ <*Gik, Gij*>) by A81, TOPREAL3: 19;

 then ( LSeg (pion1,1)) c= ( LSeg (Gik,Gij)) by SPPOL_2: 21;

 then

 A96: (( LSeg (go,(( len go) -' 1))) /\ ( LSeg (pion1,1))) c= {Gik} by A44, A51, XBOOLE_1: 27;



 A97: ( len pion1) >= (1 + 1) by A84, FINSEQ_1: 44;

 {Gik} c= (( LSeg (go,m)) /\ ( LSeg (pion1,1)))

 proof

 let x be object;

 assume x in {Gik};

 then

 A98: x = Gik by TARSKI:def 1;



 A99: Gik in ( LSeg (go,m)) by A48, RLTOPSP1: 68;

 Gik in ( LSeg (pion1,1)) by A41, A92, A97, TOPREAL1: 21;

 hence thesis by A98, A99, XBOOLE_0:def 4;

 end;

 then (( LSeg (go,(( len go) -' 1))) /\ ( LSeg (pion1,1))) = {(go /. ( len go))} by A41, A44, A96;

 then

 A100: (go ^' pion1) is unfolded by A92, TOPREAL8: 34;

 ( len pion1) >= (2 + 0 ) by A84, FINSEQ_1: 44;

 then

 A101: (( len pion1) - 2) >= 0 by XREAL_1: 19;

 ((( len (go ^' pion1)) + 1) - 1) = ((( len go) + ( len pion1)) - 1) by FINSEQ_6: 139;



 then (( len (go ^' pion1)) - 1) = (( len go) + (( len pion1) - 2))

 .= (( len go) + (( len pion1) -' 2)) by A101, XREAL_0:def 2;

 then

 A102: (( len (go ^' pion1)) -' 1) = (( len go) + (( len pion1) -' 2)) by XREAL_0:def 2;



 A103: (( len pion1) - 1) >= 1 by A97, XREAL_1: 19;

 then

 A104: (( len pion1) -' 1) = (( len pion1) - 1) by XREAL_0:def 2;



 A105: ((( len pion1) -' 2) + 1) = ((( len pion1) - 2) + 1) by A101, XREAL_0:def 2

 .= (( len pion1) -' 1) by A103, XREAL_0:def 2;

 ((( len pion1) - 1) + 1) <= ( len pion1);

 then

 A106: (( len pion1) -' 1) < ( len pion1) by A104, NAT_1: 13;

 ( LSeg (pion1,(( len pion1) -' 1))) c= ( L~ <*Gik, Gij*>) by A81, TOPREAL3: 19;

 then ( LSeg (pion1,(( len pion1) -' 1))) c= ( LSeg (Gik,Gij)) by SPPOL_2: 21;

 then

 A107: (( LSeg (pion1,(( len pion1) -' 1))) /\ ( LSeg (co,1))) c= {Gij} by A58, XBOOLE_1: 27;

 {Gij} c= (( LSeg (pion1,(( len pion1) -' 1))) /\ ( LSeg (co,1)))

 proof

 let x be object;

 assume x in {Gij};

 then

 A108: x = Gij by TARSKI:def 1;

 (pion1 /. ((( len pion1) -' 1) + 1)) = (pion /. 2) by A83, A104, FINSEQ_1: 44

 .= Gij by FINSEQ_4: 17;

 then

 A109: Gij in ( LSeg (pion1,(( len pion1) -' 1))) by A103, A104, TOPREAL1: 21;

 Gij in ( LSeg (co,1)) by A55, RLTOPSP1: 68;

 hence thesis by A108, A109, XBOOLE_0:def 4;

 end;

 then (( LSeg (pion1,(( len pion1) -' 1))) /\ ( LSeg (co,1))) = {Gij} by A107;

 then

 A110: (( LSeg ((go ^' pion1),(( len go) + (( len pion1) -' 2)))) /\ ( LSeg (co,1))) = {((go ^' pion1) /. ( len (go ^' pion1)))} by A42, A92, A94, A105, A106, TOPREAL8: 31;



 A111: (go ^' pion1) is non trivial by A87, NAT_D: 60;



 A112: ( rng pion1) c= ( L~ pion1) by A97, SPPOL_2: 18;



 A113: {(pion1 /. 1)} c= (( L~ go) /\ ( L~ pion1))

 proof

 let x be object;

 assume x in {(pion1 /. 1)};

 then

 A114: x = (pion1 /. 1) by TARSKI:def 1;

 then

 A115: x in ( rng pion1) by FINSEQ_6: 42;

 x in ( rng go) by A92, A114, FINSEQ_6: 168;

 hence thesis by A61, A112, A115, XBOOLE_0:def 4;

 end;

 (( L~ go) /\ ( L~ pion1)) c= {(pion1 /. 1)}

 proof

 let x be object;

 assume

 A116: x in (( L~ go) /\ ( L~ pion1));

 then

 A117: x in ( L~ pion1) by XBOOLE_0:def 4;

 x in ( L~ go) by A116, XBOOLE_0:def 4;

 then x in (( L~ pion1) /\ ( L~ US)) by A46, A117, XBOOLE_0:def 4;

 hence thesis by A6, A41, A81, A92, SPPOL_2: 21;

 end;

 then

 A118: (( L~ go) /\ ( L~ pion1)) = {(pion1 /. 1)} by A113;

 then

 A119: (go ^' pion1) is s.n.c. by A92, Th54;

 (( rng go) /\ ( rng pion1)) c= {(pion1 /. 1)} by A61, A112, A118, XBOOLE_1: 27;

 then

 A120: (go ^' pion1) is one-to-one by Th55;



 A121: (pion /. ( len pion)) = (pion /. 2) by FINSEQ_1: 44

 .= (co /. 1) by A42, FINSEQ_4: 17;



 A122: {(pion1 /. ( len pion1))} c= (( L~ co) /\ ( L~ pion1))

 proof

 let x be object;

 assume x in {(pion1 /. ( len pion1))};

 then

 A123: x = (pion1 /. ( len pion1)) by TARSKI:def 1;

 then

 A124: x in ( rng pion1) by FINSEQ_6: 168;

 x in ( rng co) by A83, A121, A123, FINSEQ_6: 42;

 hence thesis by A62, A112, A124, XBOOLE_0:def 4;

 end;

 (( L~ co) /\ ( L~ pion1)) c= {(pion1 /. ( len pion1))}

 proof

 let x be object;

 assume

 A125: x in (( L~ co) /\ ( L~ pion1));

 then

 A126: x in ( L~ pion1) by XBOOLE_0:def 4;

 x in ( L~ co) by A125, XBOOLE_0:def 4;

 then x in (( L~ pion1) /\ ( L~ LS)) by A53, A126, XBOOLE_0:def 4;

 hence thesis by A7, A42, A81, A83, A121, SPPOL_2: 21;

 end;

 then

 A127: (( L~ co) /\ ( L~ pion1)) = {(pion1 /. ( len pion1))} by A122;



 A128: (( L~ (go ^' pion1)) /\ ( L~ co)) = ((( L~ go) \/ ( L~ pion1)) /\ ( L~ co)) by A92, TOPREAL8: 35

 .= ( {(go /. 1)} \/ {(co /. 1)}) by A72, A83, A121, A127, XBOOLE_1: 23

 .= ( {((go ^' pion1) /. 1)} \/ {(co /. 1)}) by FINSEQ_6: 155

 .= {((go ^' pion1) /. 1), (co /. 1)} by ENUMSET1: 1;

 (co /. ( len co)) = ((go ^' pion1) /. 1) by A60, FINSEQ_6: 155;

 then

 reconsider godo as non constant standard special_circular_sequence by A90, A94, A95, A100, A102, A110, A111, A119, A120, A128, JORDAN8: 4, JORDAN8: 5, TOPREAL8: 11, TOPREAL8: 33, TOPREAL8: 34;



 A129: LA is_an_arc_of (( E-max C),( W-min C)) by JORDAN6:def 9;

 then

 A130: LA is connected by JORDAN6: 10;



 A131: ( W-min C) in LA by A129, TOPREAL1: 1;



 A132: ( E-max C) in LA by A129, TOPREAL1: 1;

 set ff = ( Rotate (( Cage (C,n)),Wmin));

 Wmin in ( rng ( Cage (C,n))) by SPRECT_2: 43;

 then

 A133: (ff /. 1) = Wmin by FINSEQ_6: 92;



 A134: ( L~ ff) = ( L~ ( Cage (C,n))) by REVROT_1: 33;

 then (( W-max ( L~ ff)) .. ff) > 1 by A133, SPRECT_5: 22;

 then (( N-min ( L~ ff)) .. ff) > 1 by A133, A134, SPRECT_5: 23, XXREAL_0: 2;

 then (( N-max ( L~ ff)) .. ff) > 1 by A133, A134, SPRECT_5: 24, XXREAL_0: 2;

 then

 A135: (Emax .. ff) > 1 by A133, A134, SPRECT_5: 25, XXREAL_0: 2;

 A136:

 now

 assume

 A137: (Gik .. US) <= 1;

 (Gik .. US) >= 1 by A34, FINSEQ_4: 21;

 then (Gik .. US) = 1 by A137, XXREAL_0: 1;

 then Gik = (US /. 1) by A34, FINSEQ_5: 38;

 hence contradiction by A18, A22, JORDAN1F: 5;

 end;



 A138: ( Cage (C,n)) is_sequence_on Ga by JORDAN9:def 1;

 then

 A139: ff is_sequence_on Ga by REVROT_1: 34;



 A140: (( right_cell (godo,1,Ga)) \ ( L~ godo)) c= ( RightComp godo) by A90, A95, JORDAN9: 27;



 A141: ( L~ godo) = (( L~ (go ^' pion1)) \/ ( L~ co)) by A94, TOPREAL8: 35

 .= ((( L~ go) \/ ( L~ pion1)) \/ ( L~ co)) by A92, TOPREAL8: 35;



 A142: ( L~ ( Cage (C,n))) = (( L~ US) \/ ( L~ LS)) by JORDAN1E: 13;

 then

 A143: ( L~ US) c= ( L~ ( Cage (C,n))) by XBOOLE_1: 7;



 A144: ( L~ LS) c= ( L~ ( Cage (C,n))) by A142, XBOOLE_1: 7;



 A145: ( L~ go) c= ( L~ ( Cage (C,n))) by A46, A143;



 A146: ( L~ co) c= ( L~ ( Cage (C,n))) by A53, A144;



 A147: ( W-min C) in C by SPRECT_1: 13;



 A148: ( L~ pion) = ( LSeg (Gik,Gij)) by SPPOL_2: 21;

 A149:

 now

 assume ( W-min C) in ( L~ godo);

 then

 A150: ( W-min C) in (( L~ go) \/ ( L~ pion1)) or ( W-min C) in ( L~ co) by A141, XBOOLE_0:def 3;

 per cases by A150, XBOOLE_0:def 3;

 suppose ( W-min C) in ( L~ go);

 then C meets ( L~ ( Cage (C,n))) by A145, A147, XBOOLE_0: 3;

 hence contradiction by JORDAN10: 5;

 end;

 suppose ( W-min C) in ( L~ pion1);

 hence contradiction by A8, A81, A131, A148, XBOOLE_0: 3;

 end;

 suppose ( W-min C) in ( L~ co);

 then C meets ( L~ ( Cage (C,n))) by A146, A147, XBOOLE_0: 3;

 hence contradiction by JORDAN10: 5;

 end;

 end;

 ( right_cell (( Rotate (( Cage (C,n)),Wmin)),1)) = ( right_cell (ff,1,( GoB ff))) by A86, JORDAN1H: 23

 .= ( right_cell (ff,1,( GoB ( Cage (C,n))))) by REVROT_1: 28

 .= ( right_cell (ff,1,Ga)) by JORDAN1H: 44

 .= ( right_cell ((ff -: Emax),1,Ga)) by A135, A139, Th53

 .= ( right_cell (US,1,Ga)) by JORDAN1E:def 1

 .= ( right_cell (( R_Cut (US,Gik)),1,Ga)) by A34, A91, A136, Th52

 .= ( right_cell ((go ^' pion1),1,Ga)) by A39, A93, Th51

 .= ( right_cell (godo,1,Ga)) by A88, A95, Th51;

 then ( W-min C) in ( right_cell (godo,1,Ga)) by JORDAN1I: 6;

 then

 A151: ( W-min C) in (( right_cell (godo,1,Ga)) \ ( L~ godo)) by A149, XBOOLE_0:def 5;



 A152: (godo /. 1) = ((go ^' pion1) /. 1) by FINSEQ_6: 155

 .= Wmin by A59, FINSEQ_6: 155;



 A153: ( len US) >= 2 by A17, XXREAL_0: 2;



 A154: (godo /. 2) = ((go ^' pion1) /. 2) by A87, FINSEQ_6: 159

 .= (US /. 2) by A33, A75, FINSEQ_6: 159

 .= ((US ^' LS) /. 2) by A153, FINSEQ_6: 159

 .= (( Rotate (( Cage (C,n)),Wmin)) /. 2) by JORDAN1E: 11;



 A155: (( L~ go) \/ ( L~ co)) is compact by COMPTS_1: 10;

 Wmin in ( rng go) by A59, FINSEQ_6: 42;

 then Wmin in (( L~ go) \/ ( L~ co)) by A61, XBOOLE_0:def 3;

 then

 A156: ( W-min (( L~ go) \/ ( L~ co))) = Wmin by A145, A146, A155, Th21, XBOOLE_1: 8;



 A157: (( W-min (( L~ go) \/ ( L~ co))) `1 ) = ( W-bound (( L~ go) \/ ( L~ co))) by EUCLID: 52;



 A158: (Wmin `1 ) = Wbo by EUCLID: 52;

 ( W-bound ( LSeg (Gik,Gij))) = (Gik `1 ) by A78, SPRECT_1: 54;

 then

 A159: ( W-bound ( L~ pion1)) = (Gik `1 ) by A81, SPPOL_2: 21;

 (Gik `1 ) >= Wbo by A10, A143, PSCOMP_1: 24;

 then (Gik `1 ) > Wbo by A74, XXREAL_0: 1;

 then ( W-min ((( L~ go) \/ ( L~ co)) \/ ( L~ pion1))) = ( W-min (( L~ go) \/ ( L~ co))) by A155, A156, A157, A158, A159, Th33;

 then

 A160: ( W-min ( L~ godo)) = Wmin by A141, A156, XBOOLE_1: 4;



 A161: ( rng godo) c= ( L~ godo) by A87, A89, SPPOL_2: 18, XXREAL_0: 2;

 2 in ( dom godo) by A90, FINSEQ_3: 25;

 then

 A162: (godo /. 2) in ( rng godo) by PARTFUN2: 2;

 (godo /. 2) in ( W-most ( L~ ( Cage (C,n)))) by A154, JORDAN1I: 25;



 then ((godo /. 2) `1 ) = (( W-min ( L~ godo)) `1 ) by A160, PSCOMP_1: 31

 .= ( W-bound ( L~ godo)) by EUCLID: 52;

 then (godo /. 2) in ( W-most ( L~ godo)) by A161, A162, SPRECT_2: 12;

 then (( Rotate (godo,( W-min ( L~ godo)))) /. 2) in ( W-most ( L~ godo)) by A152, A160, FINSEQ_6: 89;

 then

 reconsider godo as clockwise_oriented non constant standard special_circular_sequence by JORDAN1I: 25;

 ( len US) in ( dom US) by FINSEQ_5: 6;



 then

 A163: (US . ( len US)) = (US /. ( len US)) by PARTFUN1:def 6

 .= Emax by JORDAN1F: 7;



 A164: ( east_halfline ( E-max C)) misses ( L~ go)

 proof

 assume ( east_halfline ( E-max C)) meets ( L~ go);

 then

 consider p be object such that

 A165: p in ( east_halfline ( E-max C)) and

 A166: p in ( L~ go) by XBOOLE_0: 3;

 reconsider p as Point of ( TOP-REAL 2) by A165;

 p in ( L~ US) by A46, A166;

 then p in (( east_halfline ( E-max C)) /\ ( L~ ( Cage (C,n)))) by A143, A165, XBOOLE_0:def 4;

 then

 A167: (p `1 ) = Ebo by JORDAN1A: 83, PSCOMP_1: 50;

 then

 A168: p = Emax by A46, A166, Th46;

 then Emax = Gik by A10, A163, A166, Th43;

 then (Gik `1 ) = ((Ga * (( len Ga),k)) `1 ) by A5, A13, A16, A167, A168, JORDAN1A: 71;

 hence contradiction by A2, A15, A30, JORDAN1G: 7;

 end;

 now

 assume ( east_halfline ( E-max C)) meets ( L~ godo);

 then

 A169: ( east_halfline ( E-max C)) meets (( L~ go) \/ ( L~ pion1)) or ( east_halfline ( E-max C)) meets ( L~ co) by A141, XBOOLE_1: 70;

 per cases by A169, XBOOLE_1: 70;

 suppose ( east_halfline ( E-max C)) meets ( L~ go);

 hence contradiction by A164;

 end;

 suppose ( east_halfline ( E-max C)) meets ( L~ pion1);

 then

 consider p be object such that

 A170: p in ( east_halfline ( E-max C)) and

 A171: p in ( L~ pion1) by XBOOLE_0: 3;

 reconsider p as Point of ( TOP-REAL 2) by A170;



 A172: (p `2 ) = (( E-max C) `2 ) by A170, TOPREAL1:def 11;

 (i + 1) <= ( len Ga) by A2, NAT_1: 13;

 then ((i + 1) - 1) <= (( len Ga) - 1) by XREAL_1: 9;

 then

 A173: i <= (( len Ga) -' 1) by XREAL_0:def 2;



 A174: (( len Ga) -' 1) <= ( len Ga) by NAT_D: 35;

 (p `1 ) = (Gik `1 ) by A78, A81, A148, A171, GOBOARD7: 5;

 then (p `1 ) <= ((Ga * ((( len Ga) -' 1),1)) `1 ) by A1, A5, A13, A16, A20, A173, A174, JORDAN1A: 18;

 then (p `1 ) <= ( E-bound C) by A20, JORDAN8: 12;

 then

 A175: (p `1 ) <= (( E-max C) `1 ) by EUCLID: 52;

 (p `1 ) >= (( E-max C) `1 ) by A170, TOPREAL1:def 11;

 then (p `1 ) = (( E-max C) `1 ) by A175, XXREAL_0: 1;

 then p = ( E-max C) by A172, TOPREAL3: 6;

 hence contradiction by A8, A81, A132, A148, A171, XBOOLE_0: 3;

 end;

 suppose ( east_halfline ( E-max C)) meets ( L~ co);

 then

 consider p be object such that

 A176: p in ( east_halfline ( E-max C)) and

 A177: p in ( L~ co) by XBOOLE_0: 3;

 reconsider p as Point of ( TOP-REAL 2) by A176;



 A178: (( E-max C) `2 ) = (p `2 ) by A176, TOPREAL1:def 11;

 set tt = ((( Index (p,co)) + (Gij .. LS)) -' 1);

 set RC = ( Rotate (( Cage (C,n)),Emax));



 A179: ( L~ RC) = ( L~ ( Cage (C,n))) by REVROT_1: 33;

 consider t be Nat such that

 A180: t in ( dom LS) and

 A181: (LS . t) = Gij by A37, FINSEQ_2: 10;

 1 <= t by A180, FINSEQ_3: 25;

 then

 A182: 1 < t by A32, A181, XXREAL_0: 1;

 t <= ( len LS) by A180, FINSEQ_3: 25;

 then (( Index (Gij,LS)) + 1) = t by A181, A182, JORDAN3: 12;

 then

 A183: ( len ( L_Cut (LS,Gij))) = (( len LS) - ( Index (Gij,LS))) by A9, A181, JORDAN3: 26;

 ( Index (p,co)) < ( len co) by A177, JORDAN3: 8;

 then ( Index (p,co)) < (( len LS) -' ( Index (Gij,LS))) by A183, XREAL_0:def 2;

 then (( Index (p,co)) + 1) <= (( len LS) -' ( Index (Gij,LS))) by NAT_1: 13;

 then

 A184: ( Index (p,co)) <= ((( len LS) -' ( Index (Gij,LS))) - 1) by XREAL_1: 19;



 A185: co = ( mid (LS,(Gij .. LS),( len LS))) by A37, Th37;



 A186: ( len RC) = ( len ( Cage (C,n))) by FINSEQ_6: 179;

 p in ( L~ LS) by A53, A177;

 then p in (( east_halfline ( E-max C)) /\ ( L~ ( Cage (C,n)))) by A144, A176, XBOOLE_0:def 4;

 then

 A187: (p `1 ) = Ebo by JORDAN1A: 83, PSCOMP_1: 50;



 A188: ( GoB RC) = ( GoB ( Cage (C,n))) by REVROT_1: 28

 .= Ga by JORDAN1H: 44;



 A189: (1 + 1) <= ( len LS) by A23, XXREAL_0: 2;

 then

 A190: 2 in ( dom LS) by FINSEQ_3: 25;

 consider jj2 be Nat such that

 A191: 1 <= jj2 and

 A192: jj2 <= ( width Ga) and

 A193: Emax = (Ga * (( len Ga),jj2)) by JORDAN1D: 25;



 A194: ( len Ga) >= 4 by JORDAN8: 10;

 then ( len Ga) >= 1 by XXREAL_0: 2;

 then

 A195: [( len Ga), jj2] in ( Indices Ga) by A191, A192, MATRIX_0: 30;



 A196: 1 <= ( Index (p,co)) by A177, JORDAN3: 8;

 LS = (RC -: Wmin) by JORDAN1G: 18;

 then

 A197: ( LSeg (LS,1)) = ( LSeg (RC,1)) by A189, SPPOL_2: 9;



 A198: Emax in ( rng ( Cage (C,n))) by SPRECT_2: 46;

 RC is_sequence_on Ga by A138, REVROT_1: 34;

 then

 consider ii,jj be Nat such that

 A199: [ii, (jj + 1)] in ( Indices Ga) and

 A200: [ii, jj] in ( Indices Ga) and

 A201: (RC /. 1) = (Ga * (ii,(jj + 1))) and

 A202: (RC /. (1 + 1)) = (Ga * (ii,jj)) by A85, A179, A186, A198, FINSEQ_6: 92, JORDAN1I: 23;



 A203: ((jj + 1) + 1) <> jj;



 A204: 1 <= jj by A200, MATRIX_0: 32;

 (RC /. 1) = ( E-max ( L~ RC)) by A179, A198, FINSEQ_6: 92;

 then

 A205: ii = ( len Ga) by A179, A199, A201, A193, A195, GOBOARD1: 5;

 then (ii - 1) >= (4 - 1) by A194, XREAL_1: 9;

 then

 A206: (ii - 1) >= 1 by XXREAL_0: 2;

 then

 A207: 1 <= (ii -' 1) by XREAL_0:def 2;



 A208: jj <= ( width Ga) by A200, MATRIX_0: 32;

 then

 A209: ((Ga * (( len Ga),jj)) `1 ) = Ebo by A16, A204, JORDAN1A: 71;



 A210: (jj + 1) <= ( width Ga) by A199, MATRIX_0: 32;

 (ii + 1) <> ii;

 then

 A211: ( right_cell (RC,1)) = ( cell (Ga,(ii -' 1),jj)) by A85, A186, A188, A199, A200, A201, A202, A203, GOBOARD5:def 6;



 A212: ii <= ( len Ga) by A200, MATRIX_0: 32;



 A213: 1 <= ii by A200, MATRIX_0: 32;



 A214: ii <= ( len Ga) by A199, MATRIX_0: 32;



 A215: 1 <= (jj + 1) by A199, MATRIX_0: 32;

 then

 A216: Ebo = ((Ga * (( len Ga),(jj + 1))) `1 ) by A16, A210, JORDAN1A: 71;



 A217: 1 <= ii by A199, MATRIX_0: 32;

 then

 A218: ((ii -' 1) + 1) = ii by XREAL_1: 235;

 then

 A219: (ii -' 1) < ( len Ga) by A214, NAT_1: 13;



 then

 A220: ((Ga * ((ii -' 1),(jj + 1))) `2 ) = ((Ga * (1,(jj + 1))) `2 ) by A215, A210, A207, GOBOARD5: 1

 .= ((Ga * (ii,(jj + 1))) `2 ) by A217, A214, A215, A210, GOBOARD5: 1;



 A221: ( E-max C) in ( right_cell (RC,1)) by JORDAN1I: 7;

 then

 A222: ((Ga * ((ii -' 1),jj)) `2 ) <= (( E-max C) `2 ) by A214, A210, A204, A211, A218, A206, JORDAN9: 17;



 A223: (( E-max C) `2 ) <= ((Ga * ((ii -' 1),(jj + 1))) `2 ) by A221, A214, A210, A204, A211, A218, A206, JORDAN9: 17;

 ((Ga * ((ii -' 1),jj)) `2 ) = ((Ga * (1,jj)) `2 ) by A204, A208, A207, A219, GOBOARD5: 1

 .= ((Ga * (ii,jj)) `2 ) by A213, A212, A204, A208, GOBOARD5: 1;

 then p in ( LSeg ((RC /. 1),(RC /. (1 + 1)))) by A187, A178, A201, A202, A205, A222, A223, A220, A209, A216, GOBOARD7: 7;

 then

 A224: p in ( LSeg (LS,1)) by A85, A197, A186, TOPREAL1:def 3;



 A225: (Gij .. LS) <= ( len LS) by A37, FINSEQ_4: 21;

 (Gij .. LS) <> ( len LS) by A29, A37, FINSEQ_4: 19;

 then

 A226: (Gij .. LS) < ( len LS) by A225, XXREAL_0: 1;



 A227: (( Index (Gij,LS)) + 1) = (Gij .. LS) by A32, A37, Th56;

 ( 0 + ( Index (Gij,LS))) < ( len LS) by A9, JORDAN3: 8;

 then (( len LS) - ( Index (Gij,LS))) > 0 by XREAL_1: 20;

 then ( Index (p,co)) <= ((( len LS) - ( Index (Gij,LS))) - 1) by A184, XREAL_0:def 2;

 then ( Index (p,co)) <= (( len LS) - (Gij .. LS)) by A227;

 then ( Index (p,co)) <= (( len LS) -' (Gij .. LS)) by XREAL_0:def 2;

 then

 A228: ( Index (p,co)) < ((( len LS) -' (Gij .. LS)) + 1) by NAT_1: 13;



 A229: p in ( LSeg (co,( Index (p,co)))) by A177, JORDAN3: 9;

 1 <= (Gij .. LS) by A37, FINSEQ_4: 21;

 then

 A230: ( LSeg (( mid (LS,(Gij .. LS),( len LS))),( Index (p,co)))) = ( LSeg (LS,((( Index (p,co)) + (Gij .. LS)) -' 1))) by A226, A196, A228, JORDAN4: 19;

 1 <= ( Index (Gij,LS)) by A9, JORDAN3: 8;

 then

 A231: (1 + 1) <= (Gij .. LS) by A227, XREAL_1: 7;

 then (( Index (p,co)) + (Gij .. LS)) >= ((1 + 1) + 1) by A196, XREAL_1: 7;

 then ((( Index (p,co)) + (Gij .. LS)) - 1) >= (((1 + 1) + 1) - 1) by XREAL_1: 9;

 then

 A232: tt >= (1 + 1) by XREAL_0:def 2;

 now

 per cases by A232, XXREAL_0: 1;

 suppose tt > (1 + 1);

 then ( LSeg (LS,1)) misses ( LSeg (LS,tt)) by TOPREAL1:def 7;

 hence contradiction by A224, A229, A185, A230, XBOOLE_0: 3;

 end;

 suppose

 A233: tt = (1 + 1);

 then (1 + 1) = ((( Index (p,co)) + (Gij .. LS)) - 1) by XREAL_0:def 2;

 then ((1 + 1) + 1) = (( Index (p,co)) + (Gij .. LS));

 then

 A234: (Gij .. LS) = 2 by A196, A231, JORDAN1E: 6;

 (( LSeg (LS,1)) /\ ( LSeg (LS,tt))) = {(LS /. 2)} by A23, A233, TOPREAL1:def 6;

 then p in {(LS /. 2)} by A224, A229, A185, A230, XBOOLE_0:def 4;

 then

 A235: p = (LS /. 2) by TARSKI:def 1;

 then

 A236: p in ( rng LS) by A190, PARTFUN2: 2;

 (p .. LS) = 2 by A190, A235, FINSEQ_5: 41;

 then p = Gij by A37, A234, A236, FINSEQ_5: 9;

 then (Gij `1 ) = Ebo by A235, JORDAN1G: 32;

 then (Gij `1 ) = ((Ga * (( len Ga),j)) `1 ) by A3, A12, A16, JORDAN1A: 71;

 hence contradiction by A2, A14, A67, JORDAN1G: 7;

 end;

 end;

 hence contradiction;

 end;

 end;

 then ( east_halfline ( E-max C)) c= (( L~ godo) ` ) by SUBSET_1: 23;

 then

 consider W be Subset of ( TOP-REAL 2) such that

 A237: W is_a_component_of (( L~ godo) ` ) and

 A238: ( east_halfline ( E-max C)) c= W by GOBOARD9: 3;

 not W is bounded by A238, JORDAN2C: 121, RLTOPSP1: 42;

 then W is_outside_component_of ( L~ godo) by A237, JORDAN2C:def 3;

 then W c= ( UBD ( L~ godo)) by JORDAN2C: 23;

 then

 A239: ( east_halfline ( E-max C)) c= ( UBD ( L~ godo)) by A238;

 ( E-max C) in ( east_halfline ( E-max C)) by TOPREAL1: 38;

 then ( E-max C) in ( UBD ( L~ godo)) by A239;

 then ( E-max C) in ( LeftComp godo) by GOBRD14: 36;

 then LA meets ( L~ godo) by A130, A131, A132, A140, A151, Th36;

 then

 A240: LA meets (( L~ go) \/ ( L~ pion1)) or LA meets ( L~ co) by A141, XBOOLE_1: 70;



 A241: LA c= C by JORDAN6: 61;

 per cases by A240, XBOOLE_1: 70;

 suppose LA meets ( L~ go);

 then LA meets ( L~ ( Cage (C,n))) by A46, A143, XBOOLE_1: 1, XBOOLE_1: 63;

 hence contradiction by A241, JORDAN10: 5, XBOOLE_1: 63;

 end;

 suppose LA meets ( L~ pion1);

 hence contradiction by A8, A81, A148;

 end;

 suppose LA meets ( L~ co);

 then LA meets ( L~ ( Cage (C,n))) by A53, A144, XBOOLE_1: 1, XBOOLE_1: 63;

 hence contradiction by A241, JORDAN10: 5, XBOOLE_1: 63;

 end;

 end;

 theorem :: JORDAN1J:59



 Th59: for C be Simple_closed_curve holds for i,j,k be Nat st 1 < i & i < ( len ( Gauge (C,n))) & 1 <= j & j <= k & k <= ( width ( Gauge (C,n))) & (( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) /\ ( L~ ( Upper_Seq (C,n)))) = {(( Gauge (C,n)) * (i,k))} & (( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) /\ ( L~ ( Lower_Seq (C,n)))) = {(( Gauge (C,n)) * (i,j))} holds ( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) meets ( Upper_Arc C)

 proof

 let C be Simple_closed_curve;

 let i,j,k be Nat;

 set Ga = ( Gauge (C,n));

 set US = ( Upper_Seq (C,n));

 set LS = ( Lower_Seq (C,n));

 set UA = ( Upper_Arc C);

 set Wmin = ( W-min ( L~ ( Cage (C,n))));

 set Emax = ( E-max ( L~ ( Cage (C,n))));

 set Wbo = ( W-bound ( L~ ( Cage (C,n))));

 set Ebo = ( E-bound ( L~ ( Cage (C,n))));

 set Gij = (Ga * (i,j));

 set Gik = (Ga * (i,k));

 assume that

 A1: 1 < i and

 A2: i < ( len Ga) and

 A3: 1 <= j and

 A4: j <= k and

 A5: k <= ( width Ga) and

 A6: (( LSeg (Gij,Gik)) /\ ( L~ US)) = {Gik} and

 A7: (( LSeg (Gij,Gik)) /\ ( L~ LS)) = {Gij} and

 A8: ( LSeg (Gij,Gik)) misses UA;

 Gij in {Gij} by TARSKI:def 1;

 then

 A9: Gij in ( L~ LS) by A7, XBOOLE_0:def 4;

 Gik in {Gik} by TARSKI:def 1;

 then

 A10: Gik in ( L~ US) by A6, XBOOLE_0:def 4;

 then

 A11: j <> k by A1, A2, A3, A5, A9, Th57;



 A12: j <= ( width Ga) by A4, A5, XXREAL_0: 2;



 A13: 1 <= k by A3, A4, XXREAL_0: 2;



 A14: [i, j] in ( Indices Ga) by A1, A2, A3, A12, MATRIX_0: 30;



 A15: [i, k] in ( Indices Ga) by A1, A2, A5, A13, MATRIX_0: 30;

 set go = ( R_Cut (US,Gik));

 set co = ( L_Cut (LS,Gij));



 A16: ( len Ga) = ( width Ga) by JORDAN8:def 1;



 A17: ( len US) >= 3 by JORDAN1E: 15;

 then ( len US) >= 1 by XXREAL_0: 2;

 then 1 in ( dom US) by FINSEQ_3: 25;



 then

 A18: (US . 1) = (US /. 1) by PARTFUN1:def 6

 .= Wmin by JORDAN1F: 5;



 A19: (Wmin `1 ) = Wbo by EUCLID: 52

 .= ((Ga * (1,k)) `1 ) by A5, A13, A16, JORDAN1A: 73;

 ( len Ga) >= 4 by JORDAN8: 10;

 then

 A20: ( len Ga) >= 1 by XXREAL_0: 2;

 then

 A21: [1, k] in ( Indices Ga) by A5, A13, MATRIX_0: 30;

 then

 A22: Gik <> (US . 1) by A1, A15, A18, A19, JORDAN1G: 7;

 then

 reconsider go as being_S-Seq FinSequence of ( TOP-REAL 2) by A10, JORDAN3: 35;



 A23: ( len LS) >= (1 + 2) by JORDAN1E: 15;

 then

 A24: ( len LS) >= 1 by XXREAL_0: 2;

 then

 A25: 1 in ( dom LS) by FINSEQ_3: 25;

 ( len LS) in ( dom LS) by A24, FINSEQ_3: 25;



 then

 A26: (LS . ( len LS)) = (LS /. ( len LS)) by PARTFUN1:def 6

 .= Wmin by JORDAN1F: 8;



 A27: (Wmin `1 ) = Wbo by EUCLID: 52

 .= ((Ga * (1,k)) `1 ) by A5, A13, A16, JORDAN1A: 73;



 A28: [i, j] in ( Indices Ga) by A1, A2, A3, A12, MATRIX_0: 30;

 then

 A29: Gij <> (LS . ( len LS)) by A1, A21, A26, A27, JORDAN1G: 7;

 then

 reconsider co as being_S-Seq FinSequence of ( TOP-REAL 2) by A9, JORDAN3: 34;



 A30: [( len Ga), k] in ( Indices Ga) by A5, A13, A20, MATRIX_0: 30;



 A31: (LS . 1) = (LS /. 1) by A25, PARTFUN1:def 6

 .= Emax by JORDAN1F: 6;

 (Emax `1 ) = Ebo by EUCLID: 52

 .= ((Ga * (( len Ga),k)) `1 ) by A5, A13, A16, JORDAN1A: 71;

 then

 A32: Gij <> (LS . 1) by A2, A28, A30, A31, JORDAN1G: 7;



 A33: ( len go) >= (1 + 1) by TOPREAL1:def 8;



 A34: Gik in ( rng US) by A1, A2, A5, A10, A13, Th40, JORDAN1G: 4;

 then

 A35: go is_sequence_on Ga by Th38, JORDAN1G: 4;



 A36: ( len co) >= (1 + 1) by TOPREAL1:def 8;



 A37: Gij in ( rng LS) by A1, A2, A3, A9, A12, Th40, JORDAN1G: 5;

 then

 A38: co is_sequence_on Ga by Th39, JORDAN1G: 5;

 reconsider go as non constant s.c.c. being_S-Seq FinSequence of ( TOP-REAL 2) by A33, A35, JGRAPH_1: 12, JORDAN8: 5;

 reconsider co as non constant s.c.c. being_S-Seq FinSequence of ( TOP-REAL 2) by A36, A38, JGRAPH_1: 12, JORDAN8: 5;



 A39: ( len go) > 1 by A33, NAT_1: 13;

 then

 A40: ( len go) in ( dom go) by FINSEQ_3: 25;



 then

 A41: (go /. ( len go)) = (go . ( len go)) by PARTFUN1:def 6

 .= Gik by A10, JORDAN3: 24;

 ( len co) >= 1 by A36, XXREAL_0: 2;

 then 1 in ( dom co) by FINSEQ_3: 25;



 then

 A42: (co /. 1) = (co . 1) by PARTFUN1:def 6

 .= Gij by A9, JORDAN3: 23;

 reconsider m = (( len go) - 1) as Nat by A40, FINSEQ_3: 26;



 A43: (m + 1) = ( len go);

 then

 A44: (( len go) -' 1) = m by NAT_D: 34;



 A45: ( LSeg (go,m)) c= ( L~ go) by TOPREAL3: 19;



 A46: ( L~ go) c= ( L~ US) by A10, JORDAN3: 41;

 then ( LSeg (go,m)) c= ( L~ US) by A45;

 then

 A47: (( LSeg (go,m)) /\ ( LSeg (Gik,Gij))) c= {Gik} by A6, XBOOLE_1: 26;

 m >= 1 by A33, XREAL_1: 19;

 then

 A48: ( LSeg (go,m)) = ( LSeg ((go /. m),Gik)) by A41, A43, TOPREAL1:def 3;

 {Gik} c= (( LSeg (go,m)) /\ ( LSeg (Gik,Gij)))

 proof

 let x be object;



 A49: Gik in ( LSeg (Gik,Gij)) by RLTOPSP1: 68;

 assume x in {Gik};

 then

 A50: x = Gik by TARSKI:def 1;

 Gik in ( LSeg (go,m)) by A48, RLTOPSP1: 68;

 hence thesis by A50, A49, XBOOLE_0:def 4;

 end;

 then

 A51: (( LSeg (go,m)) /\ ( LSeg (Gik,Gij))) = {Gik} by A47;



 A52: ( LSeg (co,1)) c= ( L~ co) by TOPREAL3: 19;



 A53: ( L~ co) c= ( L~ LS) by A9, JORDAN3: 42;

 then ( LSeg (co,1)) c= ( L~ LS) by A52;

 then

 A54: (( LSeg (co,1)) /\ ( LSeg (Gik,Gij))) c= {Gij} by A7, XBOOLE_1: 26;



 A55: ( LSeg (co,1)) = ( LSeg (Gij,(co /. (1 + 1)))) by A36, A42, TOPREAL1:def 3;

 {Gij} c= (( LSeg (co,1)) /\ ( LSeg (Gik,Gij)))

 proof

 let x be object;



 A56: Gij in ( LSeg (Gik,Gij)) by RLTOPSP1: 68;

 assume x in {Gij};

 then

 A57: x = Gij by TARSKI:def 1;

 Gij in ( LSeg (co,1)) by A55, RLTOPSP1: 68;

 hence thesis by A57, A56, XBOOLE_0:def 4;

 end;

 then

 A58: (( LSeg (Gik,Gij)) /\ ( LSeg (co,1))) = {Gij} by A54;



 A59: (go /. 1) = (US /. 1) by A10, SPRECT_3: 22

 .= Wmin by JORDAN1F: 5;



 then

 A60: (go /. 1) = (LS /. ( len LS)) by JORDAN1F: 8

 .= (co /. ( len co)) by A9, Th35;



 A61: ( rng go) c= ( L~ go) by A33, SPPOL_2: 18;



 A62: ( rng co) c= ( L~ co) by A36, SPPOL_2: 18;



 A63: {(go /. 1)} c= (( L~ go) /\ ( L~ co))

 proof

 let x be object;

 assume x in {(go /. 1)};

 then

 A64: x = (go /. 1) by TARSKI:def 1;

 then

 A65: x in ( rng go) by FINSEQ_6: 42;

 x in ( rng co) by A60, A64, FINSEQ_6: 168;

 hence thesis by A61, A62, A65, XBOOLE_0:def 4;

 end;



 A66: (LS . 1) = (LS /. 1) by A25, PARTFUN1:def 6

 .= Emax by JORDAN1F: 6;



 A67: [( len Ga), j] in ( Indices Ga) by A3, A12, A20, MATRIX_0: 30;

 (( L~ go) /\ ( L~ co)) c= {(go /. 1)}

 proof

 let x be object;

 assume

 A68: x in (( L~ go) /\ ( L~ co));

 then

 A69: x in ( L~ co) by XBOOLE_0:def 4;

 A70:

 now

 assume x = Emax;

 then

 A71: Emax = Gij by A9, A66, A69, JORDAN1E: 7;

 ((Ga * (( len Ga),j)) `1 ) = Ebo by A3, A12, A16, JORDAN1A: 71;

 then (Emax `1 ) <> Ebo by A2, A14, A67, A71, JORDAN1G: 7;

 hence contradiction by EUCLID: 52;

 end;

 x in ( L~ go) by A68, XBOOLE_0:def 4;

 then x in (( L~ US) /\ ( L~ LS)) by A46, A53, A69, XBOOLE_0:def 4;

 then x in {Wmin, Emax} by JORDAN1E: 16;

 then x = Wmin or x = Emax by TARSKI:def 2;

 hence thesis by A59, A70, TARSKI:def 1;

 end;

 then

 A72: (( L~ go) /\ ( L~ co)) = {(go /. 1)} by A63;

 set W2 = (go /. 2);



 A73: 2 in ( dom go) by A33, FINSEQ_3: 25;

 A74:

 now

 assume (Gik `1 ) = Wbo;

 then ((Ga * (1,k)) `1 ) = ((Ga * (i,k)) `1 ) by A5, A13, A16, JORDAN1A: 73;

 hence contradiction by A1, A15, A21, JORDAN1G: 7;

 end;

 go = ( mid (US,1,(Gik .. US))) by A34, JORDAN1G: 49

 .= (US | (Gik .. US)) by A34, FINSEQ_4: 21, FINSEQ_6: 116;

 then

 A75: W2 = (US /. 2) by A73, FINSEQ_4: 70;

 set pion = <*Gik, Gij*>;

 A76:

 now

 let n be Nat;

 assume n in ( dom pion);

 then n in ( Seg 2) by FINSEQ_1: 89;

 then n = 1 or n = 2 by FINSEQ_1: 2, TARSKI:def 2;

 hence ex i,j be Nat st [i, j] in ( Indices Ga) & (pion /. n) = (Ga * (i,j)) by A14, A15, FINSEQ_4: 17;

 end;



 A77: Gik <> Gij by A11, A14, A15, GOBOARD1: 5;



 A78: (Gik `1 ) = ((Ga * (i,1)) `1 ) by A1, A2, A5, A13, GOBOARD5: 2

 .= (Gij `1 ) by A1, A2, A3, A12, GOBOARD5: 2;

 then ( LSeg (Gik,Gij)) is vertical by SPPOL_1: 16;

 then pion is being_S-Seq by A77, JORDAN1B: 7;

 then

 consider pion1 be FinSequence of ( TOP-REAL 2) such that

 A79: pion1 is_sequence_on Ga and

 A80: pion1 is being_S-Seq and

 A81: ( L~ pion) = ( L~ pion1) and

 A82: (pion /. 1) = (pion1 /. 1) and

 A83: (pion /. ( len pion)) = (pion1 /. ( len pion1)) and

 A84: ( len pion) <= ( len pion1) by A76, GOBOARD3: 2;

 reconsider pion1 as being_S-Seq FinSequence of ( TOP-REAL 2) by A80;

 set godo = ((go ^' pion1) ^' co);



 A85: (1 + 1) <= ( len ( Cage (C,n))) by GOBOARD7: 34, XXREAL_0: 2;



 A86: (1 + 1) <= ( len ( Rotate (( Cage (C,n)),Wmin))) by GOBOARD7: 34, XXREAL_0: 2;

 ( len (go ^' pion1)) >= ( len go) by TOPREAL8: 7;

 then

 A87: ( len (go ^' pion1)) >= (1 + 1) by A33, XXREAL_0: 2;

 then

 A88: ( len (go ^' pion1)) > (1 + 0 ) by NAT_1: 13;



 A89: ( len godo) >= ( len (go ^' pion1)) by TOPREAL8: 7;

 then

 A90: (1 + 1) <= ( len godo) by A87, XXREAL_0: 2;



 A91: US is_sequence_on Ga by JORDAN1G: 4;



 A92: (go /. ( len go)) = (pion1 /. 1) by A41, A82, FINSEQ_4: 17;

 then

 A93: (go ^' pion1) is_sequence_on Ga by A35, A79, TOPREAL8: 12;



 A94: ((go ^' pion1) /. ( len (go ^' pion1))) = (pion /. ( len pion)) by A83, FINSEQ_6: 156

 .= (pion /. 2) by FINSEQ_1: 44

 .= (co /. 1) by A42, FINSEQ_4: 17;

 then

 A95: godo is_sequence_on Ga by A38, A93, TOPREAL8: 12;

 ( LSeg (pion1,1)) c= ( L~ <*Gik, Gij*>) by A81, TOPREAL3: 19;

 then ( LSeg (pion1,1)) c= ( LSeg (Gik,Gij)) by SPPOL_2: 21;

 then

 A96: (( LSeg (go,(( len go) -' 1))) /\ ( LSeg (pion1,1))) c= {Gik} by A44, A51, XBOOLE_1: 27;



 A97: ( len pion1) >= (1 + 1) by A84, FINSEQ_1: 44;

 {Gik} c= (( LSeg (go,m)) /\ ( LSeg (pion1,1)))

 proof

 let x be object;

 assume x in {Gik};

 then

 A98: x = Gik by TARSKI:def 1;



 A99: Gik in ( LSeg (go,m)) by A48, RLTOPSP1: 68;

 Gik in ( LSeg (pion1,1)) by A41, A92, A97, TOPREAL1: 21;

 hence thesis by A98, A99, XBOOLE_0:def 4;

 end;

 then (( LSeg (go,(( len go) -' 1))) /\ ( LSeg (pion1,1))) = {(go /. ( len go))} by A41, A44, A96;

 then

 A100: (go ^' pion1) is unfolded by A92, TOPREAL8: 34;

 ( len pion1) >= (2 + 0 ) by A84, FINSEQ_1: 44;

 then

 A101: (( len pion1) - 2) >= 0 by XREAL_1: 19;

 ((( len (go ^' pion1)) + 1) - 1) = ((( len go) + ( len pion1)) - 1) by FINSEQ_6: 139;



 then (( len (go ^' pion1)) - 1) = (( len go) + (( len pion1) - 2))

 .= (( len go) + (( len pion1) -' 2)) by A101, XREAL_0:def 2;

 then

 A102: (( len (go ^' pion1)) -' 1) = (( len go) + (( len pion1) -' 2)) by XREAL_0:def 2;



 A103: (( len pion1) - 1) >= 1 by A97, XREAL_1: 19;

 then

 A104: (( len pion1) -' 1) = (( len pion1) - 1) by XREAL_0:def 2;



 A105: ((( len pion1) -' 2) + 1) = ((( len pion1) - 2) + 1) by A101, XREAL_0:def 2

 .= (( len pion1) -' 1) by A103, XREAL_0:def 2;

 ((( len pion1) - 1) + 1) <= ( len pion1);

 then

 A106: (( len pion1) -' 1) < ( len pion1) by A104, NAT_1: 13;

 ( LSeg (pion1,(( len pion1) -' 1))) c= ( L~ <*Gik, Gij*>) by A81, TOPREAL3: 19;

 then ( LSeg (pion1,(( len pion1) -' 1))) c= ( LSeg (Gik,Gij)) by SPPOL_2: 21;

 then

 A107: (( LSeg (pion1,(( len pion1) -' 1))) /\ ( LSeg (co,1))) c= {Gij} by A58, XBOOLE_1: 27;

 {Gij} c= (( LSeg (pion1,(( len pion1) -' 1))) /\ ( LSeg (co,1)))

 proof

 let x be object;

 assume x in {Gij};

 then

 A108: x = Gij by TARSKI:def 1;

 (pion1 /. ((( len pion1) -' 1) + 1)) = (pion /. 2) by A83, A104, FINSEQ_1: 44

 .= Gij by FINSEQ_4: 17;

 then

 A109: Gij in ( LSeg (pion1,(( len pion1) -' 1))) by A103, A104, TOPREAL1: 21;

 Gij in ( LSeg (co,1)) by A55, RLTOPSP1: 68;

 hence thesis by A108, A109, XBOOLE_0:def 4;

 end;

 then (( LSeg (pion1,(( len pion1) -' 1))) /\ ( LSeg (co,1))) = {Gij} by A107;

 then

 A110: (( LSeg ((go ^' pion1),(( len go) + (( len pion1) -' 2)))) /\ ( LSeg (co,1))) = {((go ^' pion1) /. ( len (go ^' pion1)))} by A42, A92, A94, A105, A106, TOPREAL8: 31;



 A111: (go ^' pion1) is non trivial by A87, NAT_D: 60;



 A112: ( rng pion1) c= ( L~ pion1) by A97, SPPOL_2: 18;



 A113: {(pion1 /. 1)} c= (( L~ go) /\ ( L~ pion1))

 proof

 let x be object;

 assume x in {(pion1 /. 1)};

 then

 A114: x = (pion1 /. 1) by TARSKI:def 1;

 then

 A115: x in ( rng pion1) by FINSEQ_6: 42;

 x in ( rng go) by A92, A114, FINSEQ_6: 168;

 hence thesis by A61, A112, A115, XBOOLE_0:def 4;

 end;

 (( L~ go) /\ ( L~ pion1)) c= {(pion1 /. 1)}

 proof

 let x be object;

 assume

 A116: x in (( L~ go) /\ ( L~ pion1));

 then

 A117: x in ( L~ pion1) by XBOOLE_0:def 4;

 x in ( L~ go) by A116, XBOOLE_0:def 4;

 then x in (( L~ pion1) /\ ( L~ US)) by A46, A117, XBOOLE_0:def 4;

 hence thesis by A6, A41, A81, A92, SPPOL_2: 21;

 end;

 then

 A118: (( L~ go) /\ ( L~ pion1)) = {(pion1 /. 1)} by A113;

 then

 A119: (go ^' pion1) is s.n.c. by A92, Th54;

 (( rng go) /\ ( rng pion1)) c= {(pion1 /. 1)} by A61, A112, A118, XBOOLE_1: 27;

 then

 A120: (go ^' pion1) is one-to-one by Th55;



 A121: (pion /. ( len pion)) = (pion /. 2) by FINSEQ_1: 44

 .= (co /. 1) by A42, FINSEQ_4: 17;



 A122: {(pion1 /. ( len pion1))} c= (( L~ co) /\ ( L~ pion1))

 proof

 let x be object;

 assume x in {(pion1 /. ( len pion1))};

 then

 A123: x = (pion1 /. ( len pion1)) by TARSKI:def 1;

 then

 A124: x in ( rng pion1) by FINSEQ_6: 168;

 x in ( rng co) by A83, A121, A123, FINSEQ_6: 42;

 hence thesis by A62, A112, A124, XBOOLE_0:def 4;

 end;

 (( L~ co) /\ ( L~ pion1)) c= {(pion1 /. ( len pion1))}

 proof

 let x be object;

 assume

 A125: x in (( L~ co) /\ ( L~ pion1));

 then

 A126: x in ( L~ pion1) by XBOOLE_0:def 4;

 x in ( L~ co) by A125, XBOOLE_0:def 4;

 then x in (( L~ pion1) /\ ( L~ LS)) by A53, A126, XBOOLE_0:def 4;

 hence thesis by A7, A42, A81, A83, A121, SPPOL_2: 21;

 end;

 then

 A127: (( L~ co) /\ ( L~ pion1)) = {(pion1 /. ( len pion1))} by A122;



 A128: (( L~ (go ^' pion1)) /\ ( L~ co)) = ((( L~ go) \/ ( L~ pion1)) /\ ( L~ co)) by A92, TOPREAL8: 35

 .= ( {(go /. 1)} \/ {(co /. 1)}) by A72, A83, A121, A127, XBOOLE_1: 23

 .= ( {((go ^' pion1) /. 1)} \/ {(co /. 1)}) by FINSEQ_6: 155

 .= {((go ^' pion1) /. 1), (co /. 1)} by ENUMSET1: 1;

 (co /. ( len co)) = ((go ^' pion1) /. 1) by A60, FINSEQ_6: 155;

 then

 reconsider godo as non constant standard special_circular_sequence by A90, A94, A95, A100, A102, A110, A111, A119, A120, A128, JORDAN8: 4, JORDAN8: 5, TOPREAL8: 11, TOPREAL8: 33, TOPREAL8: 34;



 A129: UA is_an_arc_of (( W-min C),( E-max C)) by JORDAN6:def 8;

 then

 A130: UA is connected by JORDAN6: 10;



 A131: ( W-min C) in UA by A129, TOPREAL1: 1;



 A132: ( E-max C) in UA by A129, TOPREAL1: 1;

 set ff = ( Rotate (( Cage (C,n)),Wmin));

 Wmin in ( rng ( Cage (C,n))) by SPRECT_2: 43;

 then

 A133: (ff /. 1) = Wmin by FINSEQ_6: 92;



 A134: ( L~ ff) = ( L~ ( Cage (C,n))) by REVROT_1: 33;

 then (( W-max ( L~ ff)) .. ff) > 1 by A133, SPRECT_5: 22;

 then (( N-min ( L~ ff)) .. ff) > 1 by A133, A134, SPRECT_5: 23, XXREAL_0: 2;

 then (( N-max ( L~ ff)) .. ff) > 1 by A133, A134, SPRECT_5: 24, XXREAL_0: 2;

 then

 A135: (Emax .. ff) > 1 by A133, A134, SPRECT_5: 25, XXREAL_0: 2;

 A136:

 now

 assume

 A137: (Gik .. US) <= 1;

 (Gik .. US) >= 1 by A34, FINSEQ_4: 21;

 then (Gik .. US) = 1 by A137, XXREAL_0: 1;

 then Gik = (US /. 1) by A34, FINSEQ_5: 38;

 hence contradiction by A18, A22, JORDAN1F: 5;

 end;



 A138: ( Cage (C,n)) is_sequence_on Ga by JORDAN9:def 1;

 then

 A139: ff is_sequence_on Ga by REVROT_1: 34;



 A140: (( right_cell (godo,1,Ga)) \ ( L~ godo)) c= ( RightComp godo) by A90, A95, JORDAN9: 27;



 A141: ( L~ godo) = (( L~ (go ^' pion1)) \/ ( L~ co)) by A94, TOPREAL8: 35

 .= ((( L~ go) \/ ( L~ pion1)) \/ ( L~ co)) by A92, TOPREAL8: 35;



 A142: ( L~ ( Cage (C,n))) = (( L~ US) \/ ( L~ LS)) by JORDAN1E: 13;

 then

 A143: ( L~ US) c= ( L~ ( Cage (C,n))) by XBOOLE_1: 7;



 A144: ( L~ LS) c= ( L~ ( Cage (C,n))) by A142, XBOOLE_1: 7;



 A145: ( L~ go) c= ( L~ ( Cage (C,n))) by A46, A143;



 A146: ( L~ co) c= ( L~ ( Cage (C,n))) by A53, A144;



 A147: ( W-min C) in C by SPRECT_1: 13;



 A148: ( L~ pion) = ( LSeg (Gik,Gij)) by SPPOL_2: 21;

 A149:

 now

 assume ( W-min C) in ( L~ godo);

 then

 A150: ( W-min C) in (( L~ go) \/ ( L~ pion1)) or ( W-min C) in ( L~ co) by A141, XBOOLE_0:def 3;

 per cases by A150, XBOOLE_0:def 3;

 suppose ( W-min C) in ( L~ go);

 then C meets ( L~ ( Cage (C,n))) by A145, A147, XBOOLE_0: 3;

 hence contradiction by JORDAN10: 5;

 end;

 suppose ( W-min C) in ( L~ pion1);

 hence contradiction by A8, A81, A131, A148, XBOOLE_0: 3;

 end;

 suppose ( W-min C) in ( L~ co);

 then C meets ( L~ ( Cage (C,n))) by A146, A147, XBOOLE_0: 3;

 hence contradiction by JORDAN10: 5;

 end;

 end;

 ( right_cell (( Rotate (( Cage (C,n)),Wmin)),1)) = ( right_cell (ff,1,( GoB ff))) by A86, JORDAN1H: 23

 .= ( right_cell (ff,1,( GoB ( Cage (C,n))))) by REVROT_1: 28

 .= ( right_cell (ff,1,Ga)) by JORDAN1H: 44

 .= ( right_cell ((ff -: Emax),1,Ga)) by A135, A139, Th53

 .= ( right_cell (US,1,Ga)) by JORDAN1E:def 1

 .= ( right_cell (( R_Cut (US,Gik)),1,Ga)) by A34, A91, A136, Th52

 .= ( right_cell ((go ^' pion1),1,Ga)) by A39, A93, Th51

 .= ( right_cell (godo,1,Ga)) by A88, A95, Th51;

 then ( W-min C) in ( right_cell (godo,1,Ga)) by JORDAN1I: 6;

 then

 A151: ( W-min C) in (( right_cell (godo,1,Ga)) \ ( L~ godo)) by A149, XBOOLE_0:def 5;



 A152: (godo /. 1) = ((go ^' pion1) /. 1) by FINSEQ_6: 155

 .= Wmin by A59, FINSEQ_6: 155;



 A153: ( len US) >= 2 by A17, XXREAL_0: 2;



 A154: (godo /. 2) = ((go ^' pion1) /. 2) by A87, FINSEQ_6: 159

 .= (US /. 2) by A33, A75, FINSEQ_6: 159

 .= ((US ^' LS) /. 2) by A153, FINSEQ_6: 159

 .= (( Rotate (( Cage (C,n)),Wmin)) /. 2) by JORDAN1E: 11;



 A155: (( L~ go) \/ ( L~ co)) is compact by COMPTS_1: 10;

 Wmin in ( rng go) by A59, FINSEQ_6: 42;

 then Wmin in (( L~ go) \/ ( L~ co)) by A61, XBOOLE_0:def 3;

 then

 A156: ( W-min (( L~ go) \/ ( L~ co))) = Wmin by A145, A146, A155, Th21, XBOOLE_1: 8;



 A157: (( W-min (( L~ go) \/ ( L~ co))) `1 ) = ( W-bound (( L~ go) \/ ( L~ co))) by EUCLID: 52;



 A158: (Wmin `1 ) = Wbo by EUCLID: 52;

 ( W-bound ( LSeg (Gik,Gij))) = (Gik `1 ) by A78, SPRECT_1: 54;

 then

 A159: ( W-bound ( L~ pion1)) = (Gik `1 ) by A81, SPPOL_2: 21;

 (Gik `1 ) >= Wbo by A10, A143, PSCOMP_1: 24;

 then (Gik `1 ) > Wbo by A74, XXREAL_0: 1;

 then ( W-min ((( L~ go) \/ ( L~ co)) \/ ( L~ pion1))) = ( W-min (( L~ go) \/ ( L~ co))) by A155, A156, A157, A158, A159, Th33;

 then

 A160: ( W-min ( L~ godo)) = Wmin by A141, A156, XBOOLE_1: 4;



 A161: ( rng godo) c= ( L~ godo) by A87, A89, SPPOL_2: 18, XXREAL_0: 2;

 2 in ( dom godo) by A90, FINSEQ_3: 25;

 then

 A162: (godo /. 2) in ( rng godo) by PARTFUN2: 2;

 (godo /. 2) in ( W-most ( L~ ( Cage (C,n)))) by A154, JORDAN1I: 25;



 then ((godo /. 2) `1 ) = (( W-min ( L~ godo)) `1 ) by A160, PSCOMP_1: 31

 .= ( W-bound ( L~ godo)) by EUCLID: 52;

 then (godo /. 2) in ( W-most ( L~ godo)) by A161, A162, SPRECT_2: 12;

 then (( Rotate (godo,( W-min ( L~ godo)))) /. 2) in ( W-most ( L~ godo)) by A152, A160, FINSEQ_6: 89;

 then

 reconsider godo as clockwise_oriented non constant standard special_circular_sequence by JORDAN1I: 25;

 ( len US) in ( dom US) by FINSEQ_5: 6;



 then

 A163: (US . ( len US)) = (US /. ( len US)) by PARTFUN1:def 6

 .= Emax by JORDAN1F: 7;



 A164: ( east_halfline ( E-max C)) misses ( L~ go)

 proof

 assume ( east_halfline ( E-max C)) meets ( L~ go);

 then

 consider p be object such that

 A165: p in ( east_halfline ( E-max C)) and

 A166: p in ( L~ go) by XBOOLE_0: 3;

 reconsider p as Point of ( TOP-REAL 2) by A165;

 p in ( L~ US) by A46, A166;

 then p in (( east_halfline ( E-max C)) /\ ( L~ ( Cage (C,n)))) by A143, A165, XBOOLE_0:def 4;

 then

 A167: (p `1 ) = Ebo by JORDAN1A: 83, PSCOMP_1: 50;

 then

 A168: p = Emax by A46, A166, Th46;

 then Emax = Gik by A10, A163, A166, Th43;

 then (Gik `1 ) = ((Ga * (( len Ga),k)) `1 ) by A5, A13, A16, A167, A168, JORDAN1A: 71;

 hence contradiction by A2, A15, A30, JORDAN1G: 7;

 end;

 now

 assume ( east_halfline ( E-max C)) meets ( L~ godo);

 then

 A169: ( east_halfline ( E-max C)) meets (( L~ go) \/ ( L~ pion1)) or ( east_halfline ( E-max C)) meets ( L~ co) by A141, XBOOLE_1: 70;

 per cases by A169, XBOOLE_1: 70;

 suppose ( east_halfline ( E-max C)) meets ( L~ go);

 hence contradiction by A164;

 end;

 suppose ( east_halfline ( E-max C)) meets ( L~ pion1);

 then

 consider p be object such that

 A170: p in ( east_halfline ( E-max C)) and

 A171: p in ( L~ pion1) by XBOOLE_0: 3;

 reconsider p as Point of ( TOP-REAL 2) by A170;



 A172: (p `2 ) = (( E-max C) `2 ) by A170, TOPREAL1:def 11;

 (i + 1) <= ( len Ga) by A2, NAT_1: 13;

 then ((i + 1) - 1) <= (( len Ga) - 1) by XREAL_1: 9;

 then

 A173: i <= (( len Ga) -' 1) by XREAL_0:def 2;



 A174: (( len Ga) -' 1) <= ( len Ga) by NAT_D: 35;

 (p `1 ) = (Gik `1 ) by A78, A81, A148, A171, GOBOARD7: 5;

 then (p `1 ) <= ((Ga * ((( len Ga) -' 1),1)) `1 ) by A1, A5, A13, A16, A20, A173, A174, JORDAN1A: 18;

 then (p `1 ) <= ( E-bound C) by A20, JORDAN8: 12;

 then

 A175: (p `1 ) <= (( E-max C) `1 ) by EUCLID: 52;

 (p `1 ) >= (( E-max C) `1 ) by A170, TOPREAL1:def 11;

 then (p `1 ) = (( E-max C) `1 ) by A175, XXREAL_0: 1;

 then p = ( E-max C) by A172, TOPREAL3: 6;

 hence contradiction by A8, A81, A132, A148, A171, XBOOLE_0: 3;

 end;

 suppose ( east_halfline ( E-max C)) meets ( L~ co);

 then

 consider p be object such that

 A176: p in ( east_halfline ( E-max C)) and

 A177: p in ( L~ co) by XBOOLE_0: 3;

 reconsider p as Point of ( TOP-REAL 2) by A176;



 A178: (( E-max C) `2 ) = (p `2 ) by A176, TOPREAL1:def 11;

 set tt = ((( Index (p,co)) + (Gij .. LS)) -' 1);

 set RC = ( Rotate (( Cage (C,n)),Emax));



 A179: ( L~ RC) = ( L~ ( Cage (C,n))) by REVROT_1: 33;

 consider t be Nat such that

 A180: t in ( dom LS) and

 A181: (LS . t) = Gij by A37, FINSEQ_2: 10;

 1 <= t by A180, FINSEQ_3: 25;

 then

 A182: 1 < t by A32, A181, XXREAL_0: 1;

 t <= ( len LS) by A180, FINSEQ_3: 25;

 then (( Index (Gij,LS)) + 1) = t by A181, A182, JORDAN3: 12;

 then

 A183: ( len ( L_Cut (LS,Gij))) = (( len LS) - ( Index (Gij,LS))) by A9, A181, JORDAN3: 26;

 ( Index (p,co)) < ( len co) by A177, JORDAN3: 8;

 then ( Index (p,co)) < (( len LS) -' ( Index (Gij,LS))) by A183, XREAL_0:def 2;

 then (( Index (p,co)) + 1) <= (( len LS) -' ( Index (Gij,LS))) by NAT_1: 13;

 then

 A184: ( Index (p,co)) <= ((( len LS) -' ( Index (Gij,LS))) - 1) by XREAL_1: 19;



 A185: co = ( mid (LS,(Gij .. LS),( len LS))) by A37, Th37;



 A186: ( len RC) = ( len ( Cage (C,n))) by FINSEQ_6: 179;

 p in ( L~ LS) by A53, A177;

 then p in (( east_halfline ( E-max C)) /\ ( L~ ( Cage (C,n)))) by A144, A176, XBOOLE_0:def 4;

 then

 A187: (p `1 ) = Ebo by JORDAN1A: 83, PSCOMP_1: 50;



 A188: ( GoB RC) = ( GoB ( Cage (C,n))) by REVROT_1: 28

 .= Ga by JORDAN1H: 44;



 A189: (1 + 1) <= ( len LS) by A23, XXREAL_0: 2;

 then

 A190: 2 in ( dom LS) by FINSEQ_3: 25;

 consider jj2 be Nat such that

 A191: 1 <= jj2 and

 A192: jj2 <= ( width Ga) and

 A193: Emax = (Ga * (( len Ga),jj2)) by JORDAN1D: 25;



 A194: ( len Ga) >= 4 by JORDAN8: 10;

 then ( len Ga) >= 1 by XXREAL_0: 2;

 then

 A195: [( len Ga), jj2] in ( Indices Ga) by A191, A192, MATRIX_0: 30;



 A196: 1 <= ( Index (p,co)) by A177, JORDAN3: 8;

 LS = (RC -: Wmin) by JORDAN1G: 18;

 then

 A197: ( LSeg (LS,1)) = ( LSeg (RC,1)) by A189, SPPOL_2: 9;



 A198: Emax in ( rng ( Cage (C,n))) by SPRECT_2: 46;

 RC is_sequence_on Ga by A138, REVROT_1: 34;

 then

 consider ii,jj be Nat such that

 A199: [ii, (jj + 1)] in ( Indices Ga) and

 A200: [ii, jj] in ( Indices Ga) and

 A201: (RC /. 1) = (Ga * (ii,(jj + 1))) and

 A202: (RC /. (1 + 1)) = (Ga * (ii,jj)) by A85, A179, A186, A198, FINSEQ_6: 92, JORDAN1I: 23;



 A203: ((jj + 1) + 1) <> jj;



 A204: 1 <= jj by A200, MATRIX_0: 32;

 (RC /. 1) = ( E-max ( L~ RC)) by A179, A198, FINSEQ_6: 92;

 then

 A205: ii = ( len Ga) by A179, A199, A201, A193, A195, GOBOARD1: 5;

 then (ii - 1) >= (4 - 1) by A194, XREAL_1: 9;

 then

 A206: (ii - 1) >= 1 by XXREAL_0: 2;

 then

 A207: 1 <= (ii -' 1) by XREAL_0:def 2;



 A208: jj <= ( width Ga) by A200, MATRIX_0: 32;

 then

 A209: ((Ga * (( len Ga),jj)) `1 ) = Ebo by A16, A204, JORDAN1A: 71;



 A210: (jj + 1) <= ( width Ga) by A199, MATRIX_0: 32;

 (ii + 1) <> ii;

 then

 A211: ( right_cell (RC,1)) = ( cell (Ga,(ii -' 1),jj)) by A85, A186, A188, A199, A200, A201, A202, A203, GOBOARD5:def 6;



 A212: ii <= ( len Ga) by A200, MATRIX_0: 32;



 A213: 1 <= ii by A200, MATRIX_0: 32;



 A214: ii <= ( len Ga) by A199, MATRIX_0: 32;



 A215: 1 <= (jj + 1) by A199, MATRIX_0: 32;

 then

 A216: Ebo = ((Ga * (( len Ga),(jj + 1))) `1 ) by A16, A210, JORDAN1A: 71;



 A217: 1 <= ii by A199, MATRIX_0: 32;

 then

 A218: ((ii -' 1) + 1) = ii by XREAL_1: 235;

 then

 A219: (ii -' 1) < ( len Ga) by A214, NAT_1: 13;



 then

 A220: ((Ga * ((ii -' 1),(jj + 1))) `2 ) = ((Ga * (1,(jj + 1))) `2 ) by A215, A210, A207, GOBOARD5: 1

 .= ((Ga * (ii,(jj + 1))) `2 ) by A217, A214, A215, A210, GOBOARD5: 1;



 A221: ( E-max C) in ( right_cell (RC,1)) by JORDAN1I: 7;

 then

 A222: ((Ga * ((ii -' 1),jj)) `2 ) <= (( E-max C) `2 ) by A214, A210, A204, A211, A218, A206, JORDAN9: 17;



 A223: (( E-max C) `2 ) <= ((Ga * ((ii -' 1),(jj + 1))) `2 ) by A221, A214, A210, A204, A211, A218, A206, JORDAN9: 17;

 ((Ga * ((ii -' 1),jj)) `2 ) = ((Ga * (1,jj)) `2 ) by A204, A208, A207, A219, GOBOARD5: 1

 .= ((Ga * (ii,jj)) `2 ) by A213, A212, A204, A208, GOBOARD5: 1;

 then p in ( LSeg ((RC /. 1),(RC /. (1 + 1)))) by A187, A178, A201, A202, A205, A222, A223, A220, A209, A216, GOBOARD7: 7;

 then

 A224: p in ( LSeg (LS,1)) by A85, A197, A186, TOPREAL1:def 3;



 A225: (Gij .. LS) <= ( len LS) by A37, FINSEQ_4: 21;

 (Gij .. LS) <> ( len LS) by A29, A37, FINSEQ_4: 19;

 then

 A226: (Gij .. LS) < ( len LS) by A225, XXREAL_0: 1;



 A227: (( Index (Gij,LS)) + 1) = (Gij .. LS) by A32, A37, Th56;

 ( 0 + ( Index (Gij,LS))) < ( len LS) by A9, JORDAN3: 8;

 then (( len LS) - ( Index (Gij,LS))) > 0 by XREAL_1: 20;

 then ( Index (p,co)) <= ((( len LS) - ( Index (Gij,LS))) - 1) by A184, XREAL_0:def 2;

 then ( Index (p,co)) <= (( len LS) - (Gij .. LS)) by A227;

 then ( Index (p,co)) <= (( len LS) -' (Gij .. LS)) by XREAL_0:def 2;

 then

 A228: ( Index (p,co)) < ((( len LS) -' (Gij .. LS)) + 1) by NAT_1: 13;



 A229: p in ( LSeg (co,( Index (p,co)))) by A177, JORDAN3: 9;

 1 <= (Gij .. LS) by A37, FINSEQ_4: 21;

 then

 A230: ( LSeg (( mid (LS,(Gij .. LS),( len LS))),( Index (p,co)))) = ( LSeg (LS,((( Index (p,co)) + (Gij .. LS)) -' 1))) by A226, A196, A228, JORDAN4: 19;

 1 <= ( Index (Gij,LS)) by A9, JORDAN3: 8;

 then

 A231: (1 + 1) <= (Gij .. LS) by A227, XREAL_1: 7;

 then (( Index (p,co)) + (Gij .. LS)) >= ((1 + 1) + 1) by A196, XREAL_1: 7;

 then ((( Index (p,co)) + (Gij .. LS)) - 1) >= (((1 + 1) + 1) - 1) by XREAL_1: 9;

 then

 A232: tt >= (1 + 1) by XREAL_0:def 2;

 now

 per cases by A232, XXREAL_0: 1;

 suppose tt > (1 + 1);

 then ( LSeg (LS,1)) misses ( LSeg (LS,tt)) by TOPREAL1:def 7;

 hence contradiction by A224, A229, A185, A230, XBOOLE_0: 3;

 end;

 suppose

 A233: tt = (1 + 1);

 then (1 + 1) = ((( Index (p,co)) + (Gij .. LS)) - 1) by XREAL_0:def 2;

 then ((1 + 1) + 1) = (( Index (p,co)) + (Gij .. LS));

 then

 A234: (Gij .. LS) = 2 by A196, A231, JORDAN1E: 6;

 (( LSeg (LS,1)) /\ ( LSeg (LS,tt))) = {(LS /. 2)} by A23, A233, TOPREAL1:def 6;

 then p in {(LS /. 2)} by A224, A229, A185, A230, XBOOLE_0:def 4;

 then

 A235: p = (LS /. 2) by TARSKI:def 1;

 then

 A236: p in ( rng LS) by A190, PARTFUN2: 2;

 (p .. LS) = 2 by A190, A235, FINSEQ_5: 41;

 then p = Gij by A37, A234, A236, FINSEQ_5: 9;

 then (Gij `1 ) = Ebo by A235, JORDAN1G: 32;

 then (Gij `1 ) = ((Ga * (( len Ga),j)) `1 ) by A3, A12, A16, JORDAN1A: 71;

 hence contradiction by A2, A14, A67, JORDAN1G: 7;

 end;

 end;

 hence contradiction;

 end;

 end;

 then ( east_halfline ( E-max C)) c= (( L~ godo) ` ) by SUBSET_1: 23;

 then

 consider W be Subset of ( TOP-REAL 2) such that

 A237: W is_a_component_of (( L~ godo) ` ) and

 A238: ( east_halfline ( E-max C)) c= W by GOBOARD9: 3;

 not W is bounded by A238, JORDAN2C: 121, RLTOPSP1: 42;

 then W is_outside_component_of ( L~ godo) by A237, JORDAN2C:def 3;

 then W c= ( UBD ( L~ godo)) by JORDAN2C: 23;

 then

 A239: ( east_halfline ( E-max C)) c= ( UBD ( L~ godo)) by A238;

 ( E-max C) in ( east_halfline ( E-max C)) by TOPREAL1: 38;

 then ( E-max C) in ( UBD ( L~ godo)) by A239;

 then ( E-max C) in ( LeftComp godo) by GOBRD14: 36;

 then UA meets ( L~ godo) by A130, A131, A132, A140, A151, Th36;

 then

 A240: UA meets (( L~ go) \/ ( L~ pion1)) or UA meets ( L~ co) by A141, XBOOLE_1: 70;



 A241: UA c= C by JORDAN6: 61;

 per cases by A240, XBOOLE_1: 70;

 suppose UA meets ( L~ go);

 then UA meets ( L~ ( Cage (C,n))) by A46, A143, XBOOLE_1: 1, XBOOLE_1: 63;

 hence contradiction by A241, JORDAN10: 5, XBOOLE_1: 63;

 end;

 suppose UA meets ( L~ pion1);

 hence contradiction by A8, A81, A148;

 end;

 suppose UA meets ( L~ co);

 then UA meets ( L~ ( Cage (C,n))) by A53, A144, XBOOLE_1: 1, XBOOLE_1: 63;

 hence contradiction by A241, JORDAN10: 5, XBOOLE_1: 63;

 end;

 end;

 theorem :: JORDAN1J:60



 Th60: for C be Simple_closed_curve holds for i,j,k be Nat st 1 0 & (( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) /\ ( Upper_Arc ( L~ ( Cage (C,n))))) = {(( Gauge (C,n)) * (i,k))} & (( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) /\ ( Lower_Arc ( L~ ( Cage (C,n))))) = {(( Gauge (C,n)) * (i,j))} holds ( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) meets ( Lower_Arc C)

 proof

 let C be Simple_closed_curve;

 let i,j,k be Nat;

 assume that

 A1: 1 0 and

 A7: (( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) /\ ( Upper_Arc ( L~ ( Cage (C,n))))) = {(( Gauge (C,n)) * (i,k))} and

 A8: (( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) /\ ( Lower_Arc ( L~ ( Cage (C,n))))) = {(( Gauge (C,n)) * (i,j))};



 A9: ( L~ ( Lower_Seq (C,n))) = ( Lower_Arc ( L~ ( Cage (C,n)))) by A6, JORDAN1G: 56;

 ( L~ ( Upper_Seq (C,n))) = ( Upper_Arc ( L~ ( Cage (C,n)))) by A6, JORDAN1G: 55;

 hence thesis by A1, A2, A3, A4, A5, A7, A8, A9, Th58;

 end;

 theorem :: JORDAN1J:61



 Th61: for C be Simple_closed_curve holds for i,j,k be Nat st 1 0 & (( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) /\ ( Upper_Arc ( L~ ( Cage (C,n))))) = {(( Gauge (C,n)) * (i,k))} & (( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) /\ ( Lower_Arc ( L~ ( Cage (C,n))))) = {(( Gauge (C,n)) * (i,j))} holds ( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) meets ( Upper_Arc C)

 proof

 let C be Simple_closed_curve;

 let i,j,k be Nat;

 assume that

 A1: 1 0 and

 A7: (( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) /\ ( Upper_Arc ( L~ ( Cage (C,n))))) = {(( Gauge (C,n)) * (i,k))} and

 A8: (( LSeg ((( Gauge (C,n)) * (i,j)),(( Gauge (C,n)) * (i,k)))) /\ ( Lower_Arc ( L~ ( Cage (C,n))))) = {(( Gauge (C,n)) * (i,j))};



 A9: ( L~ ( Lower_Seq (C,n))) = ( Lower_Arc ( L~ ( Cage (C,n)))) by A6, JORDAN1G: 56;

 ( L~ ( Upper_Seq (C,n))) = ( Upper_Arc ( L~ ( Cage (C,n)))) by A6, JORDAN1G: 55;

 hence thesis by A1, A2, A3, A4, A5, A7, A8, A9, Th59;

 end;

 theorem :: JORDAN1J:62

 for C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2) holds for j be Nat holds (( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)) in ( Upper_Arc ( L~ ( Cage (C,(n + 1))))) & 1 <= j & j <= ( width ( Gauge (C,(n + 1)))) implies ( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)))) meets ( Lower_Arc ( L~ ( Cage (C,(n + 1)))))

 proof

 let C be compact connected non vertical non horizontal Subset of ( TOP-REAL 2);

 let j be Nat;

 assume that

 A1: (( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)) in ( Upper_Arc ( L~ ( Cage (C,(n + 1))))) and

 A2: 1 <= j and

 A3: j <= ( width ( Gauge (C,(n + 1))));

 set in1 = ( Center ( Gauge (C,(n + 1))));



 A4: 1 <= in1 by JORDAN1B: 11;



 A5: ( Upper_Arc ( L~ ( Cage (C,(n + 1))))) c= ( L~ ( Cage (C,(n + 1)))) by JORDAN6: 61;



 A6: in1 <= ( len ( Gauge (C,(n + 1)))) by JORDAN1B: 13;

 (n + 1) >= ( 0 + 1) by NAT_1: 11;

 then ( LSeg ((( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),1)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)))) c= ( LSeg ((( Gauge (C,1)) * (( Center ( Gauge (C,1))),1)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)))) by A2, A3, JORDAN1A: 45;

 hence thesis by A1, A2, A3, A4, A6, A5, JORDAN1G: 57, XBOOLE_1: 63;

 end;

 theorem :: JORDAN1J:63

 for C be Simple_closed_curve holds for j,k be Nat holds 1 <= j & j <= k & k <= ( width ( Gauge (C,(n + 1)))) & (( LSeg ((( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k)))) /\ ( Upper_Arc ( L~ ( Cage (C,(n + 1)))))) = {(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k))} & (( LSeg ((( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k)))) /\ ( Lower_Arc ( L~ ( Cage (C,(n + 1)))))) = {(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j))} implies ( LSeg ((( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k)))) meets ( Lower_Arc C)

 proof

 let C be Simple_closed_curve;

 let j,k be Nat;

 assume that

 A1: 1 <= j and

 A2: j <= k and

 A3: k <= ( width ( Gauge (C,(n + 1)))) and

 A4: (( LSeg ((( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k)))) /\ ( Upper_Arc ( L~ ( Cage (C,(n + 1)))))) = {(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k))} and

 A5: (( LSeg ((( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k)))) /\ ( Lower_Arc ( L~ ( Cage (C,(n + 1)))))) = {(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j))};



 A6: ( len ( Gauge (C,(n + 1)))) >= 4 by JORDAN8: 10;

 then ( len ( Gauge (C,(n + 1)))) >= 2 by XXREAL_0: 2;

 then

 A7: 1 < ( Center ( Gauge (C,(n + 1)))) by JORDAN1B: 14;

 ( len ( Gauge (C,(n + 1)))) >= 3 by A6, XXREAL_0: 2;

 hence thesis by A1, A2, A3, A4, A5, A7, Th60, JORDAN1B: 15;

 end;

 theorem :: JORDAN1J:64

 for C be Simple_closed_curve holds for j,k be Nat holds 1 <= j & j <= k & k <= ( width ( Gauge (C,(n + 1)))) & (( LSeg ((( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k)))) /\ ( Upper_Arc ( L~ ( Cage (C,(n + 1)))))) = {(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k))} & (( LSeg ((( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k)))) /\ ( Lower_Arc ( L~ ( Cage (C,(n + 1)))))) = {(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j))} implies ( LSeg ((( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k)))) meets ( Upper_Arc C)

 proof

 let C be Simple_closed_curve;

 let j,k be Nat;

 assume that

 A1: 1 <= j and

 A2: j <= k and

 A3: k <= ( width ( Gauge (C,(n + 1)))) and

 A4: (( LSeg ((( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k)))) /\ ( Upper_Arc ( L~ ( Cage (C,(n + 1)))))) = {(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k))} and

 A5: (( LSeg ((( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j)),(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),k)))) /\ ( Lower_Arc ( L~ ( Cage (C,(n + 1)))))) = {(( Gauge (C,(n + 1))) * (( Center ( Gauge (C,(n + 1)))),j))};



 A6: ( len ( Gauge (C,(n + 1)))) >= 4 by JORDAN8: 10;

 then ( len ( Gauge (C,(n + 1)))) >= 2 by XXREAL_0: 2;

 then

 A7: 1 < ( Center ( Gauge (C,(n + 1)))) by JORDAN1B: 14;

 ( len ( Gauge (C,(n + 1)))) >= 3 by A6, XXREAL_0: 2;

 hence thesis by A1, A2, A3, A4, A5, A7, Th61, JORDAN1B: 15;

 end;

 theorem :: JORDAN1J:65

 for X,Y be non empty compact Subset of ( TOP-REAL 2) st X c= Y & (( W-min Y) in X or ( W-max Y) in X) holds ( W-bound X) = ( W-bound Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume that

 A1: X c= Y and

 A2: ( W-min Y) in X or ( W-max Y) in X;



 A3: (( W-max X) `1 ) = ( W-bound X) by EUCLID: 52;



 A4: (( W-max Y) `1 ) = ( W-bound Y) by EUCLID: 52;



 A5: (( W-min Y) `1 ) = ( W-bound Y) by EUCLID: 52;

 (( W-min X) `1 ) = ( W-bound X) by EUCLID: 52;

 hence thesis by A1, A2, A3, A5, A4, Th21, Th22;

 end;

 theorem :: JORDAN1J:66

 for X,Y be non empty compact Subset of ( TOP-REAL 2) st X c= Y & (( E-min Y) in X or ( E-max Y) in X) holds ( E-bound X) = ( E-bound Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume that

 A1: X c= Y and

 A2: ( E-min Y) in X or ( E-max Y) in X;



 A3: (( E-max X) `1 ) = ( E-bound X) by EUCLID: 52;



 A4: (( E-max Y) `1 ) = ( E-bound Y) by EUCLID: 52;



 A5: (( E-min Y) `1 ) = ( E-bound Y) by EUCLID: 52;

 (( E-min X) `1 ) = ( E-bound X) by EUCLID: 52;

 hence thesis by A1, A2, A3, A5, A4, Th17, Th18;

 end;

 theorem :: JORDAN1J:67

 for X,Y be non empty compact Subset of ( TOP-REAL 2) st X c= Y & (( N-min Y) in X or ( N-max Y) in X) holds ( N-bound X) = ( N-bound Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume that

 A1: X c= Y and

 A2: ( N-min Y) in X or ( N-max Y) in X;



 A3: (( N-max X) `2 ) = ( N-bound X) by EUCLID: 52;



 A4: (( N-max Y) `2 ) = ( N-bound Y) by EUCLID: 52;



 A5: (( N-min Y) `2 ) = ( N-bound Y) by EUCLID: 52;

 (( N-min X) `2 ) = ( N-bound X) by EUCLID: 52;

 hence thesis by A1, A2, A3, A5, A4, Th15, Th16;

 end;

 theorem :: JORDAN1J:68

 for X,Y be non empty compact Subset of ( TOP-REAL 2) st X c= Y & (( S-min Y) in X or ( S-max Y) in X) holds ( S-bound X) = ( S-bound Y)

 proof

 let X,Y be non empty compact Subset of ( TOP-REAL 2);

 assume that

 A1: X c= Y and

 A2: ( S-min Y) in X or ( S-max Y) in X;



 A3: (( S-max X) `2 ) = ( S-bound X) by EUCLID: 52;



 A4: (( S-max Y) `2 ) = ( S-bound Y) by EUCLID: 52;



 A5: (( S-min Y) `2 ) = ( S-bound Y) by EUCLID: 52;

 (( S-min X) `2 ) = ( S-bound X) by EUCLID: 52;

 hence thesis by A1, A2, A3, A5, A4, Th19, Th20;

 end;