:: JORDAN10 semantic presentation begin registration clusterV21() connected compact non horizontal non vertical for Element of K6( the carrier of (TOP-REAL 2)); existence ex b1 being Subset of (TOP-REAL 2) st ( b1 is connected & b1 is compact & not b1 is vertical & not b1 is horizontal ) proof take R^2-unit_square ; ::_thesis: ( R^2-unit_square is connected & R^2-unit_square is compact & not R^2-unit_square is vertical & not R^2-unit_square is horizontal ) thus ( R^2-unit_square is connected & R^2-unit_square is compact & not R^2-unit_square is vertical & not R^2-unit_square is horizontal ) ; ::_thesis: verum end; end; theorem Th1: :: JORDAN10:1 for k, n, i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,(j + 1)) holds i < len (Gauge (C,n)) proof let k, n, i, j be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,(j + 1)) holds i < len (Gauge (C,n)) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,(j + 1)) implies i < len (Gauge (C,n)) ) set f = Cage (C,n); set G = Gauge (C,n); assume that A1: ( 1 <= k & k + 1 <= len (Cage (C,n)) ) and A2: [i,j] in Indices (Gauge (C,n)) and A3: ( [i,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,(j + 1)) ) ; ::_thesis: i < len (Gauge (C,n)) assume A4: i >= len (Gauge (C,n)) ; ::_thesis: contradiction len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; then A5: j <= len (Gauge (C,n)) by A2, MATRIX_1:38; i <= len (Gauge (C,n)) by A2, MATRIX_1:38; then A6: i = len (Gauge (C,n)) by A4, XXREAL_0:1; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then right_cell ((Cage (C,n)),k,(Gauge (C,n))) = cell ((Gauge (C,n)),i,j) by A1, A2, A3, GOBRD13:22; hence contradiction by A1, A6, A5, JORDAN8:16, JORDAN9:31; ::_thesis: verum end; theorem Th2: :: JORDAN10:2 for k, n, i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,(j + 1)) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) holds i > 1 proof let k, n, i, j be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,(j + 1)) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) holds i > 1 let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,(j + 1)) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) implies i > 1 ) set f = Cage (C,n); set G = Gauge (C,n); assume that A1: ( 1 <= k & k + 1 <= len (Cage (C,n)) ) and A2: [i,j] in Indices (Gauge (C,n)) and A3: ( [i,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,(j + 1)) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) ) ; ::_thesis: i > 1 assume A4: i <= 1 ; ::_thesis: contradiction 1 <= i by A2, MATRIX_1:38; then i = 1 by A4, XXREAL_0:1; then A5: i -' 1 = 0 by XREAL_1:232; len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; then A6: j <= len (Gauge (C,n)) by A2, MATRIX_1:38; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then right_cell ((Cage (C,n)),k,(Gauge (C,n))) = cell ((Gauge (C,n)),(i -' 1),j) by A1, A2, A3, GOBRD13:28; hence contradiction by A1, A5, A6, JORDAN8:18, JORDAN9:31; ::_thesis: verum end; theorem Th3: :: JORDAN10:3 for k, n, i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * ((i + 1),j) holds j > 1 proof let k, n, i, j be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * ((i + 1),j) holds j > 1 let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * ((i + 1),j) implies j > 1 ) set f = Cage (C,n); set G = Gauge (C,n); assume that A1: ( 1 <= k & k + 1 <= len (Cage (C,n)) ) and A2: [i,j] in Indices (Gauge (C,n)) and A3: ( [(i + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * ((i + 1),j) ) ; ::_thesis: j > 1 assume A4: j <= 1 ; ::_thesis: contradiction 1 <= j by A2, MATRIX_1:38; then j = 1 by A4, XXREAL_0:1; then A5: j -' 1 = 0 by XREAL_1:232; A6: i <= len (Gauge (C,n)) by A2, MATRIX_1:38; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then right_cell ((Cage (C,n)),k,(Gauge (C,n))) = cell ((Gauge (C,n)),i,(j -' 1)) by A1, A2, A3, GOBRD13:24; hence contradiction by A1, A5, A6, JORDAN8:17, JORDAN9:31; ::_thesis: verum end; theorem Th4: :: JORDAN10:4 for k, n, i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((i + 1),j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) holds j < width (Gauge (C,n)) proof let k, n, i, j be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((i + 1),j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) holds j < width (Gauge (C,n)) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((i + 1),j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) implies j < width (Gauge (C,n)) ) set f = Cage (C,n); set G = Gauge (C,n); assume that A1: ( 1 <= k & k + 1 <= len (Cage (C,n)) ) and A2: [i,j] in Indices (Gauge (C,n)) and A3: ( [(i + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((i + 1),j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) ) ; ::_thesis: j < width (Gauge (C,n)) assume A4: j >= width (Gauge (C,n)) ; ::_thesis: contradiction j <= width (Gauge (C,n)) by A2, MATRIX_1:38; then A5: j = width (Gauge (C,n)) by A4, XXREAL_0:1; A6: ( len (Gauge (C,n)) = width (Gauge (C,n)) & i <= len (Gauge (C,n)) ) by A2, JORDAN8:def_1, MATRIX_1:38; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then right_cell ((Cage (C,n)),k,(Gauge (C,n))) = cell ((Gauge (C,n)),i,j) by A1, A2, A3, GOBRD13:26; hence contradiction by A1, A5, A6, JORDAN8:15, JORDAN9:31; ::_thesis: verum end; theorem Th5: :: JORDAN10:5 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses L~ (Cage (C,n)) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses L~ (Cage (C,n)) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: C misses L~ (Cage (C,n)) set f = Cage (C,n); set G = Gauge (C,n); assume not C misses L~ (Cage (C,n)) ; ::_thesis: contradiction then consider c being set such that A1: c in C and A2: c in L~ (Cage (C,n)) by XBOOLE_0:3; L~ (Cage (C,n)) = union { (LSeg ((Cage (C,n)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (Cage (C,n)) ) } by TOPREAL1:def_4; then consider Z being set such that A3: c in Z and A4: Z in { (LSeg ((Cage (C,n)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (Cage (C,n)) ) } by A2, TARSKI:def_4; consider i being Element of NAT such that A5: Z = LSeg ((Cage (C,n)),i) and A6: ( 1 <= i & i + 1 <= len (Cage (C,n)) ) by A4; Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then LSeg ((Cage (C,n)),i) = (left_cell ((Cage (C,n)),i,(Gauge (C,n)))) /\ (right_cell ((Cage (C,n)),i,(Gauge (C,n)))) by A6, GOBRD13:29; then A7: c in left_cell ((Cage (C,n)),i,(Gauge (C,n))) by A3, A5, XBOOLE_0:def_4; left_cell ((Cage (C,n)),i,(Gauge (C,n))) misses C by A6, JORDAN9:31; hence contradiction by A1, A7, XBOOLE_0:3; ::_thesis: verum end; theorem Th6: :: JORDAN10:6 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) set a = N-bound C; set s = S-bound C; set w = W-bound C; set f = Cage (C,n); set G = Gauge (C,n); consider i being Element of NAT such that A1: 1 <= i and A2: i + 1 <= len (Gauge (C,n)) and A3: (Cage (C,n)) /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) and (Cage (C,n)) /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) and N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) and N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) by JORDAN9:def_1; A4: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; 4 <= len (Gauge (C,n)) by JORDAN8:10; then A5: 1 <= len (Gauge (C,n)) by XXREAL_0:2; i + 0 <= i + 1 by XREAL_1:6; then i <= len (Gauge (C,n)) by A2, XXREAL_0:2; then A6: [i,(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A1, A4, A5, MATRIX_1:36; A7: 2 |^ n <> 0 by NEWTON:83; thus N-bound (L~ (Cage (C,n))) = (N-min (L~ (Cage (C,n)))) `2 by EUCLID:52 .= ((Cage (C,n)) /. 1) `2 by JORDAN9:32 .= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2)))]| `2 by A3, A4, A6, JORDAN8:def_1 .= (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2)) by EUCLID:52 .= (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((2 |^ n) + 3) - 2)) by JORDAN8:def_1 .= ((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (2 |^ n))) + (((N-bound C) - (S-bound C)) / (2 |^ n)) .= ((S-bound C) + ((N-bound C) - (S-bound C))) + (((N-bound C) - (S-bound C)) / (2 |^ n)) by A7, XCMPLX_1:87 .= (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) ; ::_thesis: verum end; theorem Th7: :: JORDAN10:7 for i, j being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i))) proof let i, j be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i))) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( i < j implies N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i))) ) assume A1: i < j ; ::_thesis: N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i))) defpred S1[ Element of NAT ] means ( i < $1 implies N-bound (L~ (Cage (C,$1))) < N-bound (L~ (Cage (C,i))) ); A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: S1[n] ; ::_thesis: S1[n + 1] set j = n + 1; set a = N-bound C; set s = S-bound C; A4: ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ (n + 1)))) - ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))) = (0 + (((N-bound C) - (S-bound C)) / (2 |^ (n + 1)))) - (((N-bound C) - (S-bound C)) / (2 |^ n)) .= (((N-bound C) - (S-bound C)) / ((2 |^ n) * 2)) - ((((N-bound C) - (S-bound C)) / (2 |^ n)) / (2 / 2)) by NEWTON:6 .= (((N-bound C) - (S-bound C)) / ((2 |^ n) * 2)) - ((((N-bound C) - (S-bound C)) * 2) / ((2 |^ n) * 2)) by XCMPLX_1:84 .= (((N-bound C) - (S-bound C)) - ((2 * (N-bound C)) - (2 * (S-bound C)))) / ((2 |^ n) * 2) by XCMPLX_1:120 .= ((S-bound C) - (N-bound C)) / ((2 |^ n) * 2) ; 2 |^ n > 0 by NEWTON:83; then A5: (2 |^ n) * 2 > 0 * 2 by XREAL_1:68; A6: ( N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) & N-bound (L~ (Cage (C,(n + 1)))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ (n + 1))) ) by Th6; (S-bound C) - (N-bound C) < 0 by SPRECT_1:32, XREAL_1:49; then 0 > ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ (n + 1)))) - ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))) by A5, A4, XREAL_1:141; then A7: N-bound (L~ (Cage (C,(n + 1)))) < N-bound (L~ (Cage (C,n))) by A6, XREAL_1:48; assume i < n + 1 ; ::_thesis: N-bound (L~ (Cage (C,(n + 1)))) < N-bound (L~ (Cage (C,i))) then i <= n by NAT_1:13; hence N-bound (L~ (Cage (C,(n + 1)))) < N-bound (L~ (Cage (C,i))) by A3, A7, XXREAL_0:1, XXREAL_0:2; ::_thesis: verum end; A8: S1[ 0 ] by NAT_1:2; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A2); hence N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i))) by A1; ::_thesis: verum end; registration let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); let n be Element of NAT ; cluster Cl (RightComp (Cage (C,n))) -> compact ; coherence Cl (RightComp (Cage (C,n))) is compact by GOBRD14:32; end; theorem Th8: :: JORDAN10:8 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-min C in RightComp (Cage (C,n)) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-min C in RightComp (Cage (C,n)) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: N-min C in RightComp (Cage (C,n)) set f = Cage (C,n); set G = Gauge (C,n); consider k being Element of NAT such that A1: 1 <= k and A2: k + 1 <= len (Gauge (C,n)) and A3: ( (Cage (C,n)) /. 1 = (Gauge (C,n)) * (k,(width (Gauge (C,n)))) & (Cage (C,n)) /. 2 = (Gauge (C,n)) * ((k + 1),(width (Gauge (C,n)))) ) and A4: N-min C in cell ((Gauge (C,n)),k,((width (Gauge (C,n))) -' 1)) and N-min C <> (Gauge (C,n)) * (k,((width (Gauge (C,n))) -' 1)) by JORDAN9:def_1; A5: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; A6: 1 <= k + 1 by NAT_1:11; then A7: 1 <= len (Gauge (C,n)) by A2, XXREAL_0:2; then A8: [(k + 1),(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A2, A5, A6, MATRIX_1:36; L~ (Cage (C,n)) <> {} ; then A9: ( Cage (C,n) is_sequence_on Gauge (C,n) & 1 + 1 <= len (Cage (C,n)) ) by GOBRD14:2, JORDAN9:def_1; then right_cell ((Cage (C,n)),1,(Gauge (C,n))) is closed by GOBRD13:30; then Fr (right_cell ((Cage (C,n)),1,(Gauge (C,n)))) = (right_cell ((Cage (C,n)),1,(Gauge (C,n)))) \ (Int (right_cell ((Cage (C,n)),1,(Gauge (C,n))))) by TOPS_1:43; then A10: (Fr (right_cell ((Cage (C,n)),1,(Gauge (C,n))))) \/ (Int (right_cell ((Cage (C,n)),1,(Gauge (C,n))))) = right_cell ((Cage (C,n)),1,(Gauge (C,n))) by TOPS_1:16, XBOOLE_1:45; A11: k < len (Gauge (C,n)) by A2, NAT_1:13; then [k,(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A1, A5, A7, MATRIX_1:36; then A12: cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)) = right_cell ((Cage (C,n)),1,(Gauge (C,n))) by A3, A9, A5, A8, GOBRD13:24; A13: Int (right_cell ((Cage (C,n)),1)) c= RightComp (Cage (C,n)) by GOBOARD9:def_2; Int (right_cell ((Cage (C,n)),1,(Gauge (C,n)))) c= Int (right_cell ((Cage (C,n)),1)) by A9, GOBRD13:33, TOPS_1:19; then A14: Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) c= RightComp (Cage (C,n)) by A12, A13, XBOOLE_1:1; RightComp (Cage (C,n)) misses L~ (Cage (C,n)) by SPRECT_3:25; then A15: (RightComp (Cage (C,n))) /\ (L~ (Cage (C,n))) = {} by XBOOLE_0:def_7; A16: Fr (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) c= (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Fr (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) or q in (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) ) assume A17: q in Fr (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) ; ::_thesis: q in (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) then reconsider s = q as Point of (TOP-REAL 2) ; 4 <= len (Gauge (C,n)) by JORDAN8:10; then 4 - 1 <= (len (Gauge (C,n))) - 1 by XREAL_1:13; then 0 <= (len (Gauge (C,n))) - 1 by XXREAL_0:2; then A18: (len (Gauge (C,n))) -' 1 = (len (Gauge (C,n))) - 1 by XREAL_0:def_2; A19: (len (Gauge (C,n))) - 1 < (len (Gauge (C,n))) - 0 by XREAL_1:15; then Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) <> {} by A5, A11, A18, GOBOARD9:14; then consider p being set such that A20: p in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by XBOOLE_0:def_1; reconsider p = p as Point of (TOP-REAL 2) by A20; percases ( q in L~ (Cage (C,n)) or not q in L~ (Cage (C,n)) ) ; suppose q in L~ (Cage (C,n)) ; ::_thesis: q in (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) hence q in (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) by XBOOLE_0:def_3; ::_thesis: verum end; supposeA21: not q in L~ (Cage (C,n)) ; ::_thesis: q in (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) A22: LSeg (p,s) c= (L~ (Cage (C,n))) ` proof 3 <= (len (Gauge (C,n))) -' 1 by GOBRD14:7; then A23: 1 <= (len (Gauge (C,n))) -' 1 by XXREAL_0:2; then A24: Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) = { |[x,y]| where x, y is Real : ( ((Gauge (C,n)) * (k,1)) `1 < x & x < ((Gauge (C,n)) * ((k + 1),1)) `1 & ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < y & y < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 ) } by A1, A5, A11, A18, A19, GOBOARD6:26; A25: cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)) = { |[m,o]| where m, o is Real : ( ((Gauge (C,n)) * (k,1)) `1 <= m & m <= ((Gauge (C,n)) * ((k + 1),1)) `1 & ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 <= o & o <= ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 ) } by A1, A5, A11, A18, A19, A23, GOBRD11:32; Fr (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) c= cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)) by A9, A12, GOBRD13:30, TOPS_1:35; then q in cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1)) by A17; then consider m, o being Real such that A26: s = |[m,o]| and A27: ((Gauge (C,n)) * (k,1)) `1 <= m and A28: m <= ((Gauge (C,n)) * ((k + 1),1)) `1 and A29: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 <= o and A30: o <= ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A25; A31: s `2 = o by A26, EUCLID:52; consider x, y being Real such that A32: p = |[x,y]| and A33: ((Gauge (C,n)) * (k,1)) `1 < x and A34: x < ((Gauge (C,n)) * ((k + 1),1)) `1 and A35: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < y and A36: y < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A20, A24; A37: p `1 = x by A32, EUCLID:52; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (p,s) or a in (L~ (Cage (C,n))) ` ) assume A38: a in LSeg (p,s) ; ::_thesis: a in (L~ (Cage (C,n))) ` then reconsider b = a as Point of (TOP-REAL 2) ; A39: b = |[(b `1),(b `2)]| by EUCLID:53; A40: p `2 = y by A32, EUCLID:52; A41: s `1 = m by A26, EUCLID:52; now__::_thesis:_(_(_b_=_s_&_a_in_(L~_(Cage_(C,n)))_`_)_or_(_b_<>_s_&_a_in_(L~_(Cage_(C,n)))_`_)_) percases ( b = s or b <> s ) ; case b = s ; ::_thesis: a in (L~ (Cage (C,n))) ` hence a in (L~ (Cage (C,n))) ` by A21, SUBSET_1:29; ::_thesis: verum end; caseA42: b <> s ; ::_thesis: a in (L~ (Cage (C,n))) ` now__::_thesis:_(_(_s_`1_<_p_`1_&_s_`2_<_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_<_p_`1_&_s_`2_>_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_<_p_`1_&_s_`2_=_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_>_p_`1_&_s_`2_<_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_>_p_`1_&_s_`2_>_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_>_p_`1_&_s_`2_=_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_=_p_`1_&_s_`2_>_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_=_p_`1_&_s_`2_<_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_or_(_s_`1_=_p_`1_&_s_`2_=_p_`2_&_b_in_Int_(cell_((Gauge_(C,n)),k,((len_(Gauge_(C,n)))_-'_1)))_)_) percases ( ( s `1 < p `1 & s `2 < p `2 ) or ( s `1 < p `1 & s `2 > p `2 ) or ( s `1 < p `1 & s `2 = p `2 ) or ( s `1 > p `1 & s `2 < p `2 ) or ( s `1 > p `1 & s `2 > p `2 ) or ( s `1 > p `1 & s `2 = p `2 ) or ( s `1 = p `1 & s `2 > p `2 ) or ( s `1 = p `1 & s `2 < p `2 ) or ( s `1 = p `1 & s `2 = p `2 ) ) by XXREAL_0:1; caseA43: ( s `1 < p `1 & s `2 < p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) then s `2 < b `2 by A38, A42, TOPREAL6:30; then A44: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < b `2 by A29, A31, XXREAL_0:2; b `1 <= p `1 by A38, A43, TOPREAL6:29; then A45: b `1 < ((Gauge (C,n)) * ((k + 1),1)) `1 by A34, A37, XXREAL_0:2; b `2 <= p `2 by A38, A43, TOPREAL6:30; then A46: b `2 < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A36, A40, XXREAL_0:2; s `1 < b `1 by A38, A42, A43, TOPREAL6:29; then ((Gauge (C,n)) * (k,1)) `1 < b `1 by A27, A41, XXREAL_0:2; hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A45, A44, A46; ::_thesis: verum end; caseA47: ( s `1 < p `1 & s `2 > p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) then b `2 < s `2 by A38, A42, TOPREAL6:30; then A48: b `2 < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A30, A31, XXREAL_0:2; b `1 <= p `1 by A38, A47, TOPREAL6:29; then A49: b `1 < ((Gauge (C,n)) * ((k + 1),1)) `1 by A34, A37, XXREAL_0:2; p `2 <= b `2 by A38, A47, TOPREAL6:30; then A50: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < b `2 by A35, A40, XXREAL_0:2; s `1 < b `1 by A38, A42, A47, TOPREAL6:29; then ((Gauge (C,n)) * (k,1)) `1 < b `1 by A27, A41, XXREAL_0:2; hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A49, A50, A48; ::_thesis: verum end; caseA51: ( s `1 < p `1 & s `2 = p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) then b `1 <= p `1 by A38, TOPREAL6:29; then A52: b `1 < ((Gauge (C,n)) * ((k + 1),1)) `1 by A34, A37, XXREAL_0:2; s `1 < b `1 by A38, A42, A51, TOPREAL6:29; then A53: ((Gauge (C,n)) * (k,1)) `1 < b `1 by A27, A41, XXREAL_0:2; p `2 = b `2 by A38, A51, GOBOARD7:6; hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A35, A36, A40, A53, A52; ::_thesis: verum end; caseA54: ( s `1 > p `1 & s `2 < p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) then s `2 < b `2 by A38, A42, TOPREAL6:30; then A55: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < b `2 by A29, A31, XXREAL_0:2; b `1 >= p `1 by A38, A54, TOPREAL6:29; then A56: ((Gauge (C,n)) * (k,1)) `1 < b `1 by A33, A37, XXREAL_0:2; b `2 <= p `2 by A38, A54, TOPREAL6:30; then A57: b `2 < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A36, A40, XXREAL_0:2; s `1 > b `1 by A38, A42, A54, TOPREAL6:29; then b `1 < ((Gauge (C,n)) * ((k + 1),1)) `1 by A28, A41, XXREAL_0:2; hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A56, A55, A57; ::_thesis: verum end; caseA58: ( s `1 > p `1 & s `2 > p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) then s `2 > b `2 by A38, A42, TOPREAL6:30; then A59: b `2 < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A30, A31, XXREAL_0:2; b `1 >= p `1 by A38, A58, TOPREAL6:29; then A60: ((Gauge (C,n)) * (k,1)) `1 < b `1 by A33, A37, XXREAL_0:2; b `2 >= p `2 by A38, A58, TOPREAL6:30; then A61: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < b `2 by A35, A40, XXREAL_0:2; s `1 > b `1 by A38, A42, A58, TOPREAL6:29; then b `1 < ((Gauge (C,n)) * ((k + 1),1)) `1 by A28, A41, XXREAL_0:2; hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A60, A61, A59; ::_thesis: verum end; caseA62: ( s `1 > p `1 & s `2 = p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) then b `1 >= p `1 by A38, TOPREAL6:29; then A63: ((Gauge (C,n)) * (k,1)) `1 < b `1 by A33, A37, XXREAL_0:2; s `1 > b `1 by A38, A42, A62, TOPREAL6:29; then A64: b `1 < ((Gauge (C,n)) * ((k + 1),1)) `1 by A28, A41, XXREAL_0:2; b `2 = p `2 by A38, A62, GOBOARD7:6; hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A35, A36, A40, A63, A64; ::_thesis: verum end; caseA65: ( s `1 = p `1 & s `2 > p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) then b `2 >= p `2 by A38, TOPREAL6:30; then A66: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < b `2 by A35, A40, XXREAL_0:2; s `2 > b `2 by A38, A42, A65, TOPREAL6:30; then A67: b `2 < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A30, A31, XXREAL_0:2; b `1 = p `1 by A38, A65, GOBOARD7:5; hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A33, A34, A37, A66, A67; ::_thesis: verum end; caseA68: ( s `1 = p `1 & s `2 < p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) then b `2 <= p `2 by A38, TOPREAL6:30; then A69: b `2 < ((Gauge (C,n)) * (1,(((len (Gauge (C,n))) -' 1) + 1))) `2 by A36, A40, XXREAL_0:2; s `2 < b `2 by A38, A42, A68, TOPREAL6:30; then A70: ((Gauge (C,n)) * (1,((len (Gauge (C,n))) -' 1))) `2 < b `2 by A29, A31, XXREAL_0:2; b `1 = p `1 by A38, A68, GOBOARD7:5; hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A24, A39, A33, A34, A37, A70, A69; ::_thesis: verum end; case ( s `1 = p `1 & s `2 = p `2 ) ; ::_thesis: b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) then p = s by TOPREAL3:6; then LSeg (p,s) = {p} by RLTOPSP1:70; hence b in Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) by A20, A38, TARSKI:def_1; ::_thesis: verum end; end; end; then not b in L~ (Cage (C,n)) by A15, A14, XBOOLE_0:def_4; hence a in (L~ (Cage (C,n))) ` by SUBSET_1:29; ::_thesis: verum end; end; end; hence a in (L~ (Cage (C,n))) ` ; ::_thesis: verum end; A71: s in LSeg (p,s) by RLTOPSP1:68; now__::_thesis:_ex_a_being_Point_of_(TOP-REAL_2)_st_ (_a_in_{p}_&_a_in_LSeg_(p,s)_) take a = p; ::_thesis: ( a in {p} & a in LSeg (p,s) ) thus ( a in {p} & a in LSeg (p,s) ) by RLTOPSP1:68, TARSKI:def_1; ::_thesis: verum end; then A72: {p} meets LSeg (p,s) by XBOOLE_0:3; ( RightComp (Cage (C,n)) is_a_component_of (L~ (Cage (C,n))) ` & {p} c= RightComp (Cage (C,n)) ) by A14, A20, GOBOARD9:def_2, ZFMISC_1:31; then LSeg (p,s) c= RightComp (Cage (C,n)) by A22, A72, GOBOARD9:4; hence q in (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) by A71, XBOOLE_0:def_3; ::_thesis: verum end; end; end; C misses L~ (Cage (C,n)) by Th5; then ( N-min C in C & C /\ (L~ (Cage (C,n))) = {} ) by SPRECT_1:11, XBOOLE_0:def_7; then A73: not N-min C in L~ (Cage (C,n)) by XBOOLE_0:def_4; RightComp (Cage (C,n)) c= (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) by XBOOLE_1:7; then Int (cell ((Gauge (C,n)),k,((len (Gauge (C,n))) -' 1))) c= (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) by A14, XBOOLE_1:1; then right_cell ((Cage (C,n)),1,(Gauge (C,n))) c= (RightComp (Cage (C,n))) \/ (L~ (Cage (C,n))) by A12, A16, A10, XBOOLE_1:8; hence N-min C in RightComp (Cage (C,n)) by A73, A4, A5, A12, XBOOLE_0:def_3; ::_thesis: verum end; theorem Th9: :: JORDAN10:9 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C meets RightComp (Cage (C,n)) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C meets RightComp (Cage (C,n)) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: C meets RightComp (Cage (C,n)) ( N-min C in C & N-min C in RightComp (Cage (C,n)) ) by Th8, SPRECT_1:11; then C /\ (RightComp (Cage (C,n))) <> {} by XBOOLE_0:def_4; hence C meets RightComp (Cage (C,n)) by XBOOLE_0:def_7; ::_thesis: verum end; theorem Th10: :: JORDAN10:10 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses LeftComp (Cage (C,n)) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses LeftComp (Cage (C,n)) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: C misses LeftComp (Cage (C,n)) set f = Cage (C,n); assume A1: C meets LeftComp (Cage (C,n)) ; ::_thesis: contradiction RightComp (Cage (C,n)) is_a_component_of (L~ (Cage (C,n))) ` by GOBOARD9:def_2; then A2: ex R being Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) st ( R = RightComp (Cage (C,n)) & R is a_component ) by CONNSP_1:def_6; C misses L~ (Cage (C,n)) by Th5; then A3: C /\ (L~ (Cage (C,n))) = {} by XBOOLE_0:def_7; C c= the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in C or c in the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) ) assume A4: c in C ; ::_thesis: c in the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) then not c in L~ (Cage (C,n)) by A3, XBOOLE_0:def_4; then c in (L~ (Cage (C,n))) ` by A4, SUBSET_1:29; hence c in the carrier of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) by PRE_TOPC:8; ::_thesis: verum end; then reconsider C1 = C as Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) ; LeftComp (Cage (C,n)) is_a_component_of (L~ (Cage (C,n))) ` by GOBOARD9:def_1; then A5: ex L being Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) st ( L = LeftComp (Cage (C,n)) & L is a_component ) by CONNSP_1:def_6; ( C meets RightComp (Cage (C,n)) & C1 is connected ) by Th9, CONNSP_1:23; hence contradiction by A1, A5, A2, JORDAN2C:92, SPRECT_4:6; ::_thesis: verum end; theorem Th11: :: JORDAN10:11 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= RightComp (Cage (C,n)) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= RightComp (Cage (C,n)) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: C c= RightComp (Cage (C,n)) set f = Cage (C,n); let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in C or c in RightComp (Cage (C,n)) ) assume A1: c in C ; ::_thesis: c in RightComp (Cage (C,n)) C misses L~ (Cage (C,n)) by Th5; then C /\ (L~ (Cage (C,n))) = {} by XBOOLE_0:def_7; then A2: not c in L~ (Cage (C,n)) by A1, XBOOLE_0:def_4; C misses LeftComp (Cage (C,n)) by Th10; then C /\ (LeftComp (Cage (C,n))) = {} by XBOOLE_0:def_7; then not c in LeftComp (Cage (C,n)) by A1, XBOOLE_0:def_4; hence c in RightComp (Cage (C,n)) by A1, A2, GOBRD14:18; ::_thesis: verum end; theorem Th12: :: JORDAN10:12 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= BDD (L~ (Cage (C,n))) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= BDD (L~ (Cage (C,n))) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: C c= BDD (L~ (Cage (C,n))) ( C c= RightComp (Cage (C,n)) & RightComp (Cage (C,n)) c= BDD (L~ (Cage (C,n))) ) by Th11, GOBRD14:35, JORDAN2C:22; hence C c= BDD (L~ (Cage (C,n))) by XBOOLE_1:1; ::_thesis: verum end; theorem Th13: :: JORDAN10:13 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD (L~ (Cage (C,n))) c= UBD C proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD (L~ (Cage (C,n))) c= UBD C let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: UBD (L~ (Cage (C,n))) c= UBD C set f = Cage (C,n); A1: UBD C = union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } by JORDAN2C:def_5; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UBD (L~ (Cage (C,n))) or x in UBD C ) A2: UBD (L~ (Cage (C,n))) = union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of L~ (Cage (C,n)) } by JORDAN2C:def_5; assume x in UBD (L~ (Cage (C,n))) ; ::_thesis: x in UBD C then consider L being set such that A3: x in L and A4: L in { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of L~ (Cage (C,n)) } by A2, TARSKI:def_4; consider B being Subset of (TOP-REAL 2) such that A5: L = B and A6: B is_outside_component_of L~ (Cage (C,n)) by A4; reconsider B1 = B as Subset of (Euclid 2) by TOPREAL3:8; A7: B1 misses RightComp (Cage (C,n)) by A6, GOBRD14:35, JORDAN2C:118; then A8: B1 /\ (RightComp (Cage (C,n))) = {} by XBOOLE_0:def_7; the carrier of ((TOP-REAL 2) | (C `)) = C ` by PRE_TOPC:8; then reconsider P1 = Component_of (Down (B,(C `))) as Subset of (TOP-REAL 2) by XBOOLE_1:1; B is_a_component_of (L~ (Cage (C,n))) ` by A6, JORDAN2C:def_3; then consider B2 being Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) such that A9: B2 = B and A10: B2 is a_component by CONNSP_1:def_6; B2 is connected by A10, CONNSP_1:def_5; then A11: B is connected by A9, CONNSP_1:23; A12: C c= RightComp (Cage (C,n)) by Th11; then not x in C by A3, A5, A8, XBOOLE_0:def_4; then x in C ` by A3, A5, XBOOLE_0:def_5; then A13: x in B /\ (C `) by A3, A5, XBOOLE_0:def_4; not B is bounded by A6, JORDAN2C:def_3; then A14: not B1 is bounded by JORDAN2C:11; B1 misses C by A7, Th11, XBOOLE_1:63; then P1 is_outside_component_of C by A11, A14, JORDAN2C:63; then A15: P1 in { W where W is Subset of (TOP-REAL 2) : W is_outside_component_of C } ; B c= C ` proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in C ` ) assume A16: a in B ; ::_thesis: a in C ` then not a in C by A12, A8, XBOOLE_0:def_4; hence a in C ` by A16, XBOOLE_0:def_5; ::_thesis: verum end; then Down (B,(C `)) = B by XBOOLE_1:28; then Down (B,(C `)) c= Component_of (Down (B,(C `))) by A11, CONNSP_1:46, CONNSP_3:1; hence x in UBD C by A1, A13, A15, TARSKI:def_4; ::_thesis: verum end; definition let C be compact non horizontal non vertical Subset of (TOP-REAL 2); func UBD-Family C -> set equals :: JORDAN10:def 1 { (UBD (L~ (Cage (C,n)))) where n is Element of NAT : verum } ; coherence { (UBD (L~ (Cage (C,n)))) where n is Element of NAT : verum } is set ; func BDD-Family C -> set equals :: JORDAN10:def 2 { (Cl (BDD (L~ (Cage (C,n))))) where n is Element of NAT : verum } ; coherence { (Cl (BDD (L~ (Cage (C,n))))) where n is Element of NAT : verum } is set ; end; :: deftheorem defines UBD-Family JORDAN10:def_1_:_ for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD-Family C = { (UBD (L~ (Cage (C,n)))) where n is Element of NAT : verum } ; :: deftheorem defines BDD-Family JORDAN10:def_2_:_ for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD-Family C = { (Cl (BDD (L~ (Cage (C,n))))) where n is Element of NAT : verum } ; definition let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: original: UBD-Family redefine func UBD-Family C -> Subset-Family of (TOP-REAL 2); coherence UBD-Family C is Subset-Family of (TOP-REAL 2) proof { (UBD (L~ (Cage (C,i)))) where i is Element of NAT : verum } c= bool the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (UBD (L~ (Cage (C,i)))) where i is Element of NAT : verum } or x in bool the carrier of (TOP-REAL 2) ) assume x in { (UBD (L~ (Cage (C,i)))) where i is Element of NAT : verum } ; ::_thesis: x in bool the carrier of (TOP-REAL 2) then ex i being Element of NAT st x = UBD (L~ (Cage (C,i))) ; hence x in bool the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence UBD-Family C is Subset-Family of (TOP-REAL 2) ; ::_thesis: verum end; :: original: BDD-Family redefine func BDD-Family C -> Subset-Family of (TOP-REAL 2); coherence BDD-Family C is Subset-Family of (TOP-REAL 2) proof { (Cl (BDD (L~ (Cage (C,i))))) where i is Element of NAT : verum } c= bool the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Cl (BDD (L~ (Cage (C,i))))) where i is Element of NAT : verum } or x in bool the carrier of (TOP-REAL 2) ) assume x in { (Cl (BDD (L~ (Cage (C,i))))) where i is Element of NAT : verum } ; ::_thesis: x in bool the carrier of (TOP-REAL 2) then ex i being Element of NAT st x = Cl (BDD (L~ (Cage (C,i)))) ; hence x in bool the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence BDD-Family C is Subset-Family of (TOP-REAL 2) ; ::_thesis: verum end; end; registration let C be compact non horizontal non vertical Subset of (TOP-REAL 2); cluster UBD-Family C -> non empty ; coherence not UBD-Family C is empty proof UBD (L~ (Cage (C,0))) in UBD-Family C ; hence not UBD-Family C is empty ; ::_thesis: verum end; cluster BDD-Family C -> non empty ; coherence not BDD-Family C is empty proof Cl (BDD (L~ (Cage (C,0)))) in BDD-Family C ; hence not BDD-Family C is empty ; ::_thesis: verum end; end; theorem Th14: :: JORDAN10:14 for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds union (UBD-Family C) = UBD C proof let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: union (UBD-Family C) = UBD C A1: ( UBD (L~ (Cage (C,0))) c= UBD C & UBD (L~ (Cage (C,0))) = LeftComp (Cage (C,0)) ) by Th13, GOBRD14:36; for X being set st X in UBD-Family C holds X c= UBD C proof let X be set ; ::_thesis: ( X in UBD-Family C implies X c= UBD C ) assume X in UBD-Family C ; ::_thesis: X c= UBD C then ex n being Element of NAT st X = UBD (L~ (Cage (C,n))) ; hence X c= UBD C by Th13; ::_thesis: verum end; hence union (UBD-Family C) c= UBD C by ZFMISC_1:76; :: according to XBOOLE_0:def_10 ::_thesis: UBD C c= union (UBD-Family C) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UBD C or x in union (UBD-Family C) ) assume A2: x in UBD C ; ::_thesis: x in union (UBD-Family C) UBD C = union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } by JORDAN2C:def_5; then consider A being set such that A3: x in A and A4: A in { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } by A2, TARSKI:def_4; ex B being Subset of (TOP-REAL 2) st ( A = B & B is_outside_component_of C ) by A4; then reconsider p = x as Point of (TOP-REAL 2) by A3; consider q being Point of (TOP-REAL 2) such that A5: q `2 > N-bound (L~ (Cage (C,0))) and A6: p <> q by TOPREAL6:33; (Cage (C,0)) /. 1 = N-min (L~ (Cage (C,0))) by JORDAN9:32; then q in LeftComp (Cage (C,0)) by A5, JORDAN2C:113; then consider P being Subset of (TOP-REAL 2) such that A7: P is_S-P_arc_joining p,q and A8: P c= UBD C by A2, A6, A1, TOPREAL4:29; consider f being FinSequence of (TOP-REAL 2) such that A9: f is being_S-Seq and A10: P = L~ f and A11: p = f /. 1 and q = f /. (len f) by A7, TOPREAL4:def_1; reconsider f = f as being_S-Seq FinSequence of (TOP-REAL 2) by A9; 2 <= len f by NAT_D:60; then A12: x in P by A10, A11, JORDAN3:1; ( not L~ f is empty & TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) ) by EUCLID:def_8; then reconsider P1 = P, C1 = C as non empty compact Subset of (TopSpaceMetr (Euclid 2)) by A10, COMPTS_1:23; set d = min_dist_min (P1,C1); UBD C is_outside_component_of C by JORDAN2C:68; then UBD C is_a_component_of C ` by JORDAN2C:def_3; then C misses UBD C by JORDAN2C:117; then P misses C by A8, XBOOLE_1:63; then min_dist_min (P1,C1) > 0 by JGRAPH_1:38; then (min_dist_min (P1,C1)) / 2 > 0 by XREAL_1:139; then consider n being Element of NAT such that 1 < n and A13: ( dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < (min_dist_min (P1,C1)) / 2 & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < (min_dist_min (P1,C1)) / 2 ) by GOBRD14:11; set G = Gauge (C,n); set g = Cage (C,n); A14: UBD (L~ (Cage (C,n))) in UBD-Family C ; A15: now__::_thesis:_not_(L~_(Cage_(C,n)))_/\_P_<>_{} assume (L~ (Cage (C,n))) /\ P <> {} ; ::_thesis: contradiction then consider a being set such that A16: a in (L~ (Cage (C,n))) /\ P by XBOOLE_0:def_1; a in L~ (Cage (C,n)) by A16, XBOOLE_0:def_4; then consider i being Element of NAT such that A17: ( 1 <= i & i + 1 <= len (Cage (C,n)) ) and A18: a in LSeg ((Cage (C,n)),i) by SPPOL_2:13; right_cell ((Cage (C,n)),i,(Gauge (C,n))) meets C by A17, JORDAN9:31; then consider c being set such that A19: c in (right_cell ((Cage (C,n)),i,(Gauge (C,n)))) /\ C by XBOOLE_0:4; reconsider c = c as Point of (Euclid 2) by A19, TOPREAL3:8; reconsider a9 = a as Point of (Euclid 2) by A16, TOPREAL3:8; A20: c in C by A19, XBOOLE_0:def_4; reconsider c9 = c as Point of (TOP-REAL 2) by A19; A21: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1; then consider i1, j1, i2, j2 being Element of NAT such that A22: [i1,j1] in Indices (Gauge (C,n)) and A23: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,j1) and A24: [i2,j2] in Indices (Gauge (C,n)) and A25: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i2,j2) and A26: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A17, JORDAN8:3; (left_cell ((Cage (C,n)),i,(Gauge (C,n)))) /\ (right_cell ((Cage (C,n)),i,(Gauge (C,n)))) = LSeg ((Cage (C,n)),i) by A17, A21, GOBRD13:29; then A27: a in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A18, XBOOLE_0:def_4; a in P by A16, XBOOLE_0:def_4; then A28: dist (a9,c) >= min_dist_min (P1,C1) by A20, WEIERSTR:34; reconsider A = a as Point of (TOP-REAL 2) by A16; set e = E-bound C; set w = W-bound C; set p = N-bound C; set s = S-bound C; A29: 4 <= len (Gauge (C,n)) by JORDAN8:10; then A30: 1 <= len (Gauge (C,n)) by XXREAL_0:2; A31: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1; then A32: 1 <= width (Gauge (C,n)) by A29, XXREAL_0:2; A33: [1,1] in Indices (Gauge (C,n)) by A31, A30, MATRIX_1:36; A34: c in right_cell ((Cage (C,n)),i,(Gauge (C,n))) by A19, XBOOLE_0:def_4; now__::_thesis:_(_(_i1_=_i2_&_j1_+_1_=_j2_&_dist_(A,c9)_<=_(((N-bound_C)_-_(S-bound_C))_/_(2_|^_n))_+_(((E-bound_C)_-_(W-bound_C))_/_(2_|^_n))_)_or_(_i1_+_1_=_i2_&_j1_=_j2_&_dist_(A,c9)_<=_(((N-bound_C)_-_(S-bound_C))_/_(2_|^_n))_+_(((E-bound_C)_-_(W-bound_C))_/_(2_|^_n))_)_or_(_i1_=_i2_+_1_&_j1_=_j2_&_dist_(A,c9)_<=_(((N-bound_C)_-_(S-bound_C))_/_(2_|^_n))_+_(((E-bound_C)_-_(W-bound_C))_/_(2_|^_n))_)_or_(_i1_=_i2_&_j1_=_j2_+_1_&_dist_(A,c9)_<=_(((N-bound_C)_-_(S-bound_C))_/_(2_|^_n))_+_(((E-bound_C)_-_(W-bound_C))_/_(2_|^_n))_)_) percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A26; caseA35: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) then A36: i1 < len (Gauge (C,n)) by A17, A22, A23, A24, A25, Th1; then A37: i1 + 1 <= len (Gauge (C,n)) by NAT_1:13; A38: 1 <= i1 by A22, MATRIX_1:38; then 1 <= i1 + 1 by NAT_1:13; then A39: [(i1 + 1),1] in Indices (Gauge (C,n)) by A32, A37, MATRIX_1:36; [i1,1] in Indices (Gauge (C,n)) by A32, A38, A36, MATRIX_1:36; then A40: ( dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) = (((Gauge (C,n)) * ((i1 + 1),1)) `1) - (((Gauge (C,n)) * (i1,1)) `1) & dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A39, GOBRD14:5, GOBRD14:10; A41: j1 + 1 <= width (Gauge (C,n)) by A24, A35, MATRIX_1:38; then A42: j1 < width (Gauge (C,n)) by NAT_1:13; A43: 1 <= j1 by A22, MATRIX_1:38; then 1 <= j1 + 1 by NAT_1:13; then A44: [1,(j1 + 1)] in Indices (Gauge (C,n)) by A30, A41, MATRIX_1:36; A45: right_cell ((Cage (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) by A17, A21, A22, A23, A24, A25, A35, GOBRD13:22 .= { |[r,t]| where r, t is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A38, A36, A43, A42, GOBRD11:32 ; then consider aa, ab being Real such that A46: a = |[aa,ab]| and A47: ( ((Gauge (C,n)) * (i1,1)) `1 <= aa & aa <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= ab & ab <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A27; A48: ( A `1 = aa & A `2 = ab ) by A46, EUCLID:52; [1,j1] in Indices (Gauge (C,n)) by A30, A43, A42, MATRIX_1:36; then A49: ( dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) = (((Gauge (C,n)) * (1,(j1 + 1))) `2) - (((Gauge (C,n)) * (1,j1)) `2) & dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) ) by A44, GOBRD14:6, GOBRD14:9; consider r, t being Real such that A50: c = |[r,t]| and A51: ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A34, A45; ( c9 `1 = r & c9 `2 = t ) by A50, EUCLID:52; hence dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A51, A47, A48, A49, A40, TOPREAL6:95; ::_thesis: verum end; caseA52: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) then A53: i1 + 1 <= len (Gauge (C,n)) by A24, MATRIX_1:38; then A54: i1 < len (Gauge (C,n)) by NAT_1:13; A55: 1 <= i1 by A22, MATRIX_1:38; then 1 <= i1 + 1 by NAT_1:13; then A56: [(i1 + 1),1] in Indices (Gauge (C,n)) by A32, A53, MATRIX_1:36; [i1,1] in Indices (Gauge (C,n)) by A32, A55, A54, MATRIX_1:36; then A57: ( dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) = (((Gauge (C,n)) * ((i1 + 1),1)) `1) - (((Gauge (C,n)) * (i1,1)) `1) & dist (((Gauge (C,n)) * (i1,1)),((Gauge (C,n)) * ((i1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A56, GOBRD14:5, GOBRD14:10; A58: j2 <= width (Gauge (C,n)) by A24, MATRIX_1:38; j2 > 1 by A17, A22, A23, A24, A25, A52, Th3; then A59: j2 - 1 > 0 by XREAL_1:50; then A60: j2 - 1 = j2 -' 1 by XREAL_0:def_2; then A61: 1 <= j2 -' 1 by A59, NAT_1:14; (width (Gauge (C,n))) - 1 < (width (Gauge (C,n))) - 0 by XREAL_1:15; then A62: j2 -' 1 < width (Gauge (C,n)) by A60, A58, XREAL_1:15; then A63: [1,(j2 -' 1)] in Indices (Gauge (C,n)) by A30, A61, MATRIX_1:36; A64: right_cell ((Cage (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,(j2 -' 1)) by A17, A21, A22, A23, A24, A25, A52, GOBRD13:24 .= { |[r,t]| where r, t is Real : ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j2 -' 1))) `2 <= t & t <= ((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2 ) } by A55, A54, A61, A62, GOBRD11:32 ; then consider aa, ab being Real such that A65: a = |[aa,ab]| and A66: ( ((Gauge (C,n)) * (i1,1)) `1 <= aa & aa <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j2 -' 1))) `2 <= ab & ab <= ((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2 ) by A27; A67: ( A `1 = aa & A `2 = ab ) by A65, EUCLID:52; 1 <= (j2 -' 1) + 1 by A61, NAT_1:13; then [1,((j2 -' 1) + 1)] in Indices (Gauge (C,n)) by A30, A60, A58, MATRIX_1:36; then A68: ( dist (((Gauge (C,n)) * (1,(j2 -' 1))),((Gauge (C,n)) * (1,((j2 -' 1) + 1)))) = (((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2) - (((Gauge (C,n)) * (1,(j2 -' 1))) `2) & dist (((Gauge (C,n)) * (1,(j2 -' 1))),((Gauge (C,n)) * (1,((j2 -' 1) + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) ) by A63, GOBRD14:6, GOBRD14:9; consider r, t being Real such that A69: c = |[r,t]| and A70: ( ((Gauge (C,n)) * (i1,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i1 + 1),1)) `1 & ((Gauge (C,n)) * (1,(j2 -' 1))) `2 <= t & t <= ((Gauge (C,n)) * (1,((j2 -' 1) + 1))) `2 ) by A34, A64; ( c9 `1 = r & c9 `2 = t ) by A69, EUCLID:52; hence dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A70, A66, A67, A68, A57, TOPREAL6:95; ::_thesis: verum end; caseA71: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) A72: 1 <= j1 + 1 by NAT_1:12; A73: j1 < width (Gauge (C,n)) by A17, A22, A23, A24, A25, A71, Th4; then j1 + 1 <= width (Gauge (C,n)) by NAT_1:13; then A74: [1,(j1 + 1)] in Indices (Gauge (C,n)) by A30, A72, MATRIX_1:36; A75: 1 <= j1 by A22, MATRIX_1:38; then [1,j1] in Indices (Gauge (C,n)) by A30, A73, MATRIX_1:36; then A76: ( dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) = (((Gauge (C,n)) * (1,(j1 + 1))) `2) - (((Gauge (C,n)) * (1,j1)) `2) & dist (((Gauge (C,n)) * (1,j1)),((Gauge (C,n)) * (1,(j1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) ) by A74, GOBRD14:6, GOBRD14:9; A77: i2 + 1 <= len (Gauge (C,n)) by A22, A71, MATRIX_1:38; then A78: i2 < len (Gauge (C,n)) by NAT_1:13; A79: 1 <= i2 by A24, MATRIX_1:38; then 1 <= i2 + 1 by NAT_1:13; then A80: [(i2 + 1),1] in Indices (Gauge (C,n)) by A32, A77, MATRIX_1:36; A81: right_cell ((Cage (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j1) by A17, A21, A22, A23, A24, A25, A71, GOBRD13:26 .= { |[r,t]| where r, t is Real : ( ((Gauge (C,n)) * (i2,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) } by A79, A78, A75, A73, GOBRD11:32 ; then consider aa, ab being Real such that A82: a = |[aa,ab]| and A83: ( ((Gauge (C,n)) * (i2,1)) `1 <= aa & aa <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= ab & ab <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A27; A84: ( A `1 = aa & A `2 = ab ) by A82, EUCLID:52; [i2,1] in Indices (Gauge (C,n)) by A32, A79, A78, MATRIX_1:36; then A85: ( dist (((Gauge (C,n)) * (i2,1)),((Gauge (C,n)) * ((i2 + 1),1))) = (((Gauge (C,n)) * ((i2 + 1),1)) `1) - (((Gauge (C,n)) * (i2,1)) `1) & dist (((Gauge (C,n)) * (i2,1)),((Gauge (C,n)) * ((i2 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A80, GOBRD14:5, GOBRD14:10; consider r, t being Real such that A86: c = |[r,t]| and A87: ( ((Gauge (C,n)) * (i2,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i2 + 1),1)) `1 & ((Gauge (C,n)) * (1,j1)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j1 + 1))) `2 ) by A34, A81; ( c9 `1 = r & c9 `2 = t ) by A86, EUCLID:52; hence dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A87, A83, A84, A76, A85, TOPREAL6:95; ::_thesis: verum end; caseA88: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) then A89: j2 + 1 <= width (Gauge (C,n)) by A22, MATRIX_1:38; then A90: j2 < width (Gauge (C,n)) by NAT_1:13; A91: 1 <= j2 by A24, MATRIX_1:38; then 1 <= j2 + 1 by NAT_1:13; then A92: [1,(j2 + 1)] in Indices (Gauge (C,n)) by A30, A89, MATRIX_1:36; [1,j2] in Indices (Gauge (C,n)) by A30, A91, A90, MATRIX_1:36; then A93: ( dist (((Gauge (C,n)) * (1,j2)),((Gauge (C,n)) * (1,(j2 + 1)))) = (((Gauge (C,n)) * (1,(j2 + 1))) `2) - (((Gauge (C,n)) * (1,j2)) `2) & dist (((Gauge (C,n)) * (1,j2)),((Gauge (C,n)) * (1,(j2 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) ) by A92, GOBRD14:6, GOBRD14:9; A94: i1 <= len (Gauge (C,n)) by A22, MATRIX_1:38; i1 > 1 by A17, A22, A23, A24, A25, A88, Th2; then A95: i1 - 1 > 0 by XREAL_1:50; then A96: i1 - 1 = i1 -' 1 by XREAL_0:def_2; then A97: 1 <= i1 -' 1 by A95, NAT_1:14; (len (Gauge (C,n))) - 1 < (len (Gauge (C,n))) - 0 by XREAL_1:15; then A98: i1 -' 1 < len (Gauge (C,n)) by A96, A94, XREAL_1:15; then A99: [(i1 -' 1),1] in Indices (Gauge (C,n)) by A32, A97, MATRIX_1:36; A100: right_cell ((Cage (C,n)),i,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j2) by A17, A21, A22, A23, A24, A25, A88, GOBRD13:28 .= { |[r,t]| where r, t is Real : ( ((Gauge (C,n)) * ((i1 -' 1),1)) `1 <= r & r <= ((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 ) } by A97, A98, A91, A90, GOBRD11:32 ; then consider aa, ab being Real such that A101: a = |[aa,ab]| and A102: ( ((Gauge (C,n)) * ((i1 -' 1),1)) `1 <= aa & aa <= ((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= ab & ab <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 ) by A27; A103: ( A `1 = aa & A `2 = ab ) by A101, EUCLID:52; 1 <= (i1 -' 1) + 1 by A97, NAT_1:13; then [((i1 -' 1) + 1),1] in Indices (Gauge (C,n)) by A32, A96, A94, MATRIX_1:36; then A104: ( dist (((Gauge (C,n)) * ((i1 -' 1),1)),((Gauge (C,n)) * (((i1 -' 1) + 1),1))) = (((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1) - (((Gauge (C,n)) * ((i1 -' 1),1)) `1) & dist (((Gauge (C,n)) * ((i1 -' 1),1)),((Gauge (C,n)) * (((i1 -' 1) + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A99, GOBRD14:5, GOBRD14:10; consider r, t being Real such that A105: c = |[r,t]| and A106: ( ((Gauge (C,n)) * ((i1 -' 1),1)) `1 <= r & r <= ((Gauge (C,n)) * (((i1 -' 1) + 1),1)) `1 & ((Gauge (C,n)) * (1,j2)) `2 <= t & t <= ((Gauge (C,n)) * (1,(j2 + 1))) `2 ) by A34, A100; ( c9 `1 = r & c9 `2 = t ) by A105, EUCLID:52; hence dist (A,c9) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by A106, A102, A103, A93, A104, TOPREAL6:95; ::_thesis: verum end; end; end; then A107: dist (a9,c) <= (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) by TOPREAL6:def_1; 1 + 1 <= len (Gauge (C,n)) by A29, XXREAL_0:2; then [(1 + 1),1] in Indices (Gauge (C,n)) by A32, MATRIX_1:36; then A108: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * ((1 + 1),1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) by A33, GOBRD14:10; 1 + 1 <= width (Gauge (C,n)) by A31, A29, XXREAL_0:2; then [1,(1 + 1)] in Indices (Gauge (C,n)) by A30, MATRIX_1:36; then dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,(1 + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) by A33, GOBRD14:9; then (((N-bound C) - (S-bound C)) / (2 |^ n)) + (((E-bound C) - (W-bound C)) / (2 |^ n)) < ((min_dist_min (P1,C1)) / 2) + ((min_dist_min (P1,C1)) / 2) by A13, A108, XREAL_1:8; hence contradiction by A28, A107, XXREAL_0:2; ::_thesis: verum end; A109: P c= (L~ (Cage (C,n))) ` proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in P or a in (L~ (Cage (C,n))) ` ) assume A110: a in P ; ::_thesis: a in (L~ (Cage (C,n))) ` then not a in L~ (Cage (C,n)) by A15, XBOOLE_0:def_4; hence a in (L~ (Cage (C,n))) ` by A110, SUBSET_1:29; ::_thesis: verum end; ( 0 < n or 0 = n ) by NAT_1:2; then N-bound (L~ (Cage (C,0))) >= N-bound (L~ (Cage (C,n))) by Th7; then ( (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) & q `2 > N-bound (L~ (Cage (C,n))) ) by A5, JORDAN9:32, XXREAL_0:2; then q in LeftComp (Cage (C,n)) by JORDAN2C:113; then q in UBD (L~ (Cage (C,n))) by GOBRD14:36; then A111: {q} c= UBD (L~ (Cage (C,n))) by ZFMISC_1:31; A112: P is_an_arc_of p,q by A7, TOPREAL4:2; now__::_thesis:_ex_a_being_Point_of_(TOP-REAL_2)_st_ (_a_in_{q}_&_a_in_P_) take a = q; ::_thesis: ( a in {q} & a in P ) thus ( a in {q} & a in P ) by A112, TARSKI:def_1, TOPREAL1:1; ::_thesis: verum end; then A113: {q} meets P by XBOOLE_0:3; UBD (L~ (Cage (C,n))) is_outside_component_of L~ (Cage (C,n)) by JORDAN2C:68; then ex E being Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) st ( E = UBD (L~ (Cage (C,n))) & E is a_component & E is not bounded Subset of (Euclid 2) ) by JORDAN2C:14; then UBD (L~ (Cage (C,n))) is_a_component_of (L~ (Cage (C,n))) ` by CONNSP_1:def_6; then P c= UBD (L~ (Cage (C,n))) by A109, A112, A111, A113, GOBOARD9:4, JORDAN6:10; hence x in union (UBD-Family C) by A12, A14, TARSKI:def_4; ::_thesis: verum end; theorem Th15: :: JORDAN10:15 for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= meet (BDD-Family C) proof let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: C c= meet (BDD-Family C) for Z being set st Z in BDD-Family C holds C c= Z proof let Z be set ; ::_thesis: ( Z in BDD-Family C implies C c= Z ) assume Z in BDD-Family C ; ::_thesis: C c= Z then consider k being Element of NAT such that A1: Z = Cl (BDD (L~ (Cage (C,k)))) ; ( C c= BDD (L~ (Cage (C,k))) & BDD (L~ (Cage (C,k))) c= Cl (BDD (L~ (Cage (C,k)))) ) by Th12, PRE_TOPC:18; hence C c= Z by A1, XBOOLE_1:1; ::_thesis: verum end; hence C c= meet (BDD-Family C) by SETFAM_1:5; ::_thesis: verum end; theorem Th16: :: JORDAN10:16 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses LeftComp (Cage (C,n)) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses LeftComp (Cage (C,n)) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: BDD C misses LeftComp (Cage (C,n)) set f = Cage (C,n); assume (BDD C) /\ (LeftComp (Cage (C,n))) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being Point of (TOP-REAL 2) such that A1: x in (BDD C) /\ (LeftComp (Cage (C,n))) by SUBSET_1:4; BDD C misses UBD C by JORDAN2C:24; then A2: (BDD C) /\ (UBD C) = {} by XBOOLE_0:def_7; x in BDD C by A1, XBOOLE_0:def_4; then not x in UBD C by A2, XBOOLE_0:def_4; then A3: not x in union (UBD-Family C) by Th14; A4: x in LeftComp (Cage (C,n)) by A1, XBOOLE_0:def_4; UBD (L~ (Cage (C,n))) in { (UBD (L~ (Cage (C,k)))) where k is Element of NAT : verum } ; then not x in UBD (L~ (Cage (C,n))) by A3, TARSKI:def_4; hence contradiction by A4, GOBRD14:36; ::_thesis: verum end; theorem Th17: :: JORDAN10:17 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C c= RightComp (Cage (C,n)) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C c= RightComp (Cage (C,n)) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: BDD C c= RightComp (Cage (C,n)) set f = Cage (C,n); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BDD C or x in RightComp (Cage (C,n)) ) LeftComp (Cage (C,n)) is_outside_component_of L~ (Cage (C,n)) by GOBRD14:34; then A1: ( UBD (L~ (Cage (C,n))) = union { E where E is Subset of (TOP-REAL 2) : E is_outside_component_of L~ (Cage (C,n)) } & LeftComp (Cage (C,n)) in { E where E is Subset of (TOP-REAL 2) : E is_outside_component_of L~ (Cage (C,n)) } ) by JORDAN2C:def_5; assume A2: x in BDD C ; ::_thesis: x in RightComp (Cage (C,n)) A3: now__::_thesis:_not_x_in_Cl_(LeftComp_(Cage_(C,n))) assume x in Cl (LeftComp (Cage (C,n))) ; ::_thesis: contradiction then BDD C meets LeftComp (Cage (C,n)) by A2, PRE_TOPC:def_7; hence contradiction by Th16; ::_thesis: verum end; BDD C misses UBD C by JORDAN2C:24; then (BDD C) /\ (UBD C) = {} by XBOOLE_0:def_7; then not x in UBD C by A2, XBOOLE_0:def_4; then A4: not x in union (UBD-Family C) by Th14; UBD (L~ (Cage (C,n))) in { (UBD (L~ (Cage (C,k)))) where k is Element of NAT : verum } ; then not x in UBD (L~ (Cage (C,n))) by A4, TARSKI:def_4; then A5: not x in LeftComp (Cage (C,n)) by A1, TARSKI:def_4; L~ (Cage (C,n)) = (Cl (LeftComp (Cage (C,n)))) \ (LeftComp (Cage (C,n))) by GOBRD14:20; then not x in L~ (Cage (C,n)) by A3, XBOOLE_0:def_5; hence x in RightComp (Cage (C,n)) by A2, A5, GOBRD14:18; ::_thesis: verum end; theorem Th18: :: JORDAN10:18 for n being Element of NAT for P being Subset of (TOP-REAL 2) for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st P is_inside_component_of C holds P misses L~ (Cage (C,n)) proof let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL 2) for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st P is_inside_component_of C holds P misses L~ (Cage (C,n)) let P be Subset of (TOP-REAL 2); ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st P is_inside_component_of C holds P misses L~ (Cage (C,n)) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ( P is_inside_component_of C implies P misses L~ (Cage (C,n)) ) set f = Cage (C,n); assume P is_inside_component_of C ; ::_thesis: P misses L~ (Cage (C,n)) then A1: P c= BDD C by JORDAN2C:22; assume P /\ (L~ (Cage (C,n))) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being Point of (TOP-REAL 2) such that A2: x in P /\ (L~ (Cage (C,n))) by SUBSET_1:4; x in P by A2, XBOOLE_0:def_4; then A3: x in BDD C by A1; A4: BDD C c= RightComp (Cage (C,n)) by Th17; x in L~ (Cage (C,n)) by A2, XBOOLE_0:def_4; hence contradiction by A3, A4, GOBRD14:18; ::_thesis: verum end; theorem Th19: :: JORDAN10:19 for n being Element of NAT for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses L~ (Cage (C,n)) proof let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses L~ (Cage (C,n)) let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: BDD C misses L~ (Cage (C,n)) assume not BDD C misses L~ (Cage (C,n)) ; ::_thesis: contradiction then consider x being set such that A1: x in (BDD C) /\ (L~ (Cage (C,n))) by XBOOLE_0:4; A2: x in L~ (Cage (C,n)) by A1, XBOOLE_0:def_4; ( BDD C = union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } & x in BDD C ) by A1, JORDAN2C:def_4, XBOOLE_0:def_4; then consider Z being set such that A3: x in Z and A4: Z in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } by TARSKI:def_4; consider B being Subset of (TOP-REAL 2) such that A5: Z = B and A6: B is_inside_component_of C by A4; B misses L~ (Cage (C,n)) by A6, Th18; then B /\ (L~ (Cage (C,n))) = {} by XBOOLE_0:def_7; hence contradiction by A3, A5, A2, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th20: :: JORDAN10:20 for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds COMPLEMENT (UBD-Family C) = BDD-Family C proof let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: COMPLEMENT (UBD-Family C) = BDD-Family C for P being Subset of (TOP-REAL 2) holds ( P in BDD-Family C iff P ` in UBD-Family C ) proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P in BDD-Family C iff P ` in UBD-Family C ) thus ( P in BDD-Family C implies P ` in UBD-Family C ) ::_thesis: ( P ` in UBD-Family C implies P in BDD-Family C ) proof assume P in BDD-Family C ; ::_thesis: P ` in UBD-Family C then consider k being Element of NAT such that A1: P = Cl (BDD (L~ (Cage (C,k)))) ; P = Cl (RightComp (Cage (C,k))) by A1, GOBRD14:37; then A2: P = (RightComp (Cage (C,k))) \/ (L~ (Cage (C,k))) by GOBRD14:21; (P `) /\ ((LeftComp (Cage (C,k))) `) = (P \/ (LeftComp (Cage (C,k)))) ` by XBOOLE_1:53 .= ([#] the carrier of (TOP-REAL 2)) ` by A2, GOBRD14:15 .= {} the carrier of (TOP-REAL 2) by XBOOLE_1:37 ; then A3: P ` misses (LeftComp (Cage (C,k))) ` by XBOOLE_0:def_7; ( L~ (Cage (C,k)) misses LeftComp (Cage (C,k)) & RightComp (Cage (C,k)) misses LeftComp (Cage (C,k)) ) by GOBRD14:14, SPRECT_3:26; then P misses LeftComp (Cage (C,k)) by A2, XBOOLE_1:70; then P ` = LeftComp (Cage (C,k)) by A3, SUBSET_1:25; then P ` = UBD (L~ (Cage (C,k))) by GOBRD14:36; hence P ` in UBD-Family C ; ::_thesis: verum end; assume P ` in UBD-Family C ; ::_thesis: P in BDD-Family C then consider k being Element of NAT such that A4: P ` = UBD (L~ (Cage (C,k))) ; A5: P ` = LeftComp (Cage (C,k)) by A4, GOBRD14:36; then ( P ` misses RightComp (Cage (C,k)) & P ` misses L~ (Cage (C,k)) ) by GOBRD14:14, SPRECT_3:26; then P ` misses (RightComp (Cage (C,k))) \/ (L~ (Cage (C,k))) by XBOOLE_1:70; then A6: P ` misses Cl (RightComp (Cage (C,k))) by GOBRD14:21; ((P `) `) /\ ((Cl (RightComp (Cage (C,k)))) `) = ((P `) \/ (Cl (RightComp (Cage (C,k))))) ` by XBOOLE_1:53 .= ((P `) \/ ((RightComp (Cage (C,k))) \/ (L~ (Cage (C,k))))) ` by GOBRD14:21 .= ([#] the carrier of (TOP-REAL 2)) ` by A5, GOBRD14:15 .= {} the carrier of (TOP-REAL 2) by XBOOLE_1:37 ; then (P `) ` misses (Cl (RightComp (Cage (C,k)))) ` by XBOOLE_0:def_7; then (P `) ` = Cl (RightComp (Cage (C,k))) by A6, SUBSET_1:25; then P = Cl (BDD (L~ (Cage (C,k)))) by GOBRD14:37; hence P in BDD-Family C ; ::_thesis: verum end; hence COMPLEMENT (UBD-Family C) = BDD-Family C by SETFAM_1:def_7; ::_thesis: verum end; theorem :: JORDAN10:21 for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds meet (BDD-Family C) = C \/ (BDD C) proof let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: meet (BDD-Family C) = C \/ (BDD C) thus meet (BDD-Family C) c= C \/ (BDD C) :: according to XBOOLE_0:def_10 ::_thesis: C \/ (BDD C) c= meet (BDD-Family C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (BDD-Family C) or x in C \/ (BDD C) ) assume A1: x in meet (BDD-Family C) ; ::_thesis: x in C \/ (BDD C) COMPLEMENT (UBD-Family C) = BDD-Family C by Th20; then ([#] the carrier of (TOP-REAL 2)) \ (union (UBD-Family C)) = meet (BDD-Family C) by SETFAM_1:33; then not x in union (UBD-Family C) by A1, XBOOLE_0:def_5; then A2: not x in UBD C by Th14; percases ( not x in C or x in C ) ; supposeA3: not x in C ; ::_thesis: x in C \/ (BDD C) A4: (BDD C) \/ (UBD C) = C ` by JORDAN2C:27; x in C ` by A1, A3, SUBSET_1:29; then x in BDD C by A2, A4, XBOOLE_0:def_3; hence x in C \/ (BDD C) by XBOOLE_0:def_3; ::_thesis: verum end; suppose x in C ; ::_thesis: x in C \/ (BDD C) hence x in C \/ (BDD C) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; BDD C misses UBD C by JORDAN2C:24; then A5: (BDD C) /\ (UBD C) = {} by XBOOLE_0:def_7; A6: BDD C c= meet (BDD-Family C) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BDD C or x in meet (BDD-Family C) ) assume A7: x in BDD C ; ::_thesis: x in meet (BDD-Family C) then not x in UBD C by A5, XBOOLE_0:def_4; then A8: not x in union (UBD-Family C) by Th14; for Y being set st Y in BDD-Family C holds x in Y proof let Y be set ; ::_thesis: ( Y in BDD-Family C implies x in Y ) assume Y in BDD-Family C ; ::_thesis: x in Y then consider n being Element of NAT such that A9: Y = Cl (BDD (L~ (Cage (C,n)))) and verum ; LeftComp (Cage (C,n)) is_outside_component_of L~ (Cage (C,n)) by GOBRD14:34; then A10: LeftComp (Cage (C,n)) in { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of L~ (Cage (C,n)) } ; BDD C misses L~ (Cage (C,n)) by Th19; then (BDD C) /\ (L~ (Cage (C,n))) = {} by XBOOLE_0:def_7; then A11: not x in L~ (Cage (C,n)) by A7, XBOOLE_0:def_4; RightComp (Cage (C,n)) is_inside_component_of L~ (Cage (C,n)) by GOBRD14:35; then A12: RightComp (Cage (C,n)) in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of L~ (Cage (C,n)) } ; UBD (L~ (Cage (C,n))) in UBD-Family C ; then ( UBD (L~ (Cage (C,n))) = union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of L~ (Cage (C,n)) } & not x in UBD (L~ (Cage (C,n))) ) by A8, JORDAN2C:def_5, TARSKI:def_4; then not x in LeftComp (Cage (C,n)) by A10, TARSKI:def_4; then ( BDD (L~ (Cage (C,n))) = union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of L~ (Cage (C,n)) } & x in RightComp (Cage (C,n)) ) by A7, A11, GOBRD14:18, JORDAN2C:def_4; then A13: x in BDD (L~ (Cage (C,n))) by A12, TARSKI:def_4; BDD (L~ (Cage (C,n))) c= Cl (BDD (L~ (Cage (C,n)))) by PRE_TOPC:18; hence x in Y by A9, A13; ::_thesis: verum end; hence x in meet (BDD-Family C) by SETFAM_1:def_1; ::_thesis: verum end; C c= meet (BDD-Family C) by Th15; hence C \/ (BDD C) c= meet (BDD-Family C) by A6, XBOOLE_1:8; ::_thesis: verum end;