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:37;
L~ (Cage C,n) <> {} ;
then A9: ( Cage C,n is_sequence_on Gauge C,n & 1 + 1 <= len (Cage C,n) ) by GOBRD14:8, JORDAN9:def 1;
then right_cell (Cage C,n),1,(Gauge C,n) is closed by GOBRD13:31;
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:77;
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:44, 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:37;
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:25;
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:34, TOPS_1:48;
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:42;
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:13;
then 4 - 1 <= (len (Gauge C,n)) - 1 by XREAL_1:15;
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:17;
then Int (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1)) <> {} by A5, A11, A18, GOBOARD9:17;
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;
per cases ( 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;
suppose A21: 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:17;
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:29;
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:31, TOPS_1:69;
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:56;
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:56;
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:57;
A40: p `2 = y by A32, EUCLID:56;
A41: s `1 = m by A26, EUCLID:56;
now
per cases ( 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:50; :: thesis: verum
end;
case A42: b <> s ; :: thesis: a in (L~ (Cage C,n)) `
now
per cases ( ( 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;
case A43: ( 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:38;
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:37;
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:38;
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:37;
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;
case A47: ( 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:38;
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:37;
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:38;
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:37;
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;
case A51: ( 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:37;
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:37;
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;
case A54: ( 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:38;
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:37;
then A56: ((Gauge C,n) * k,1) `1 < b `1 by A33, A37, XXREAL_0:2;
b `2 <= p `2 by A38, A54, TOPREAL6:38;
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:37;
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;
case A58: ( 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:38;
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:37;
then A60: ((Gauge C,n) * k,1) `1 < b `1 by A33, A37, XXREAL_0:2;
b `2 >= p `2 by A38, A58, TOPREAL6:38;
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:37;
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;
case A62: ( 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:37;
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:37;
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;
case A65: ( 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:38;
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:38;
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;
case A68: ( 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:38;
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:38;
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:11;
then LSeg p,s = {p} by RLTOPSP1:71;
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:50; :: thesis: verum
end;
end;
end;
hence a in (L~ (Cage C,n)) ` ; :: thesis: verum
end;
A71: s in LSeg p,s by RLTOPSP1:69;
now
take a = p; :: thesis: ( a in {p} & a in LSeg p,s )
thus ( a in {p} & a in LSeg p,s ) by RLTOPSP1:69, 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:37;
then LSeg p,s c= RightComp (Cage C,n) by A22, A72, GOBOARD9:6;
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:13, 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