let n be 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 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_0:30;
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_0:30;
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;
RightComp (Cage (C,n)) misses L~ (Cage (C,n)) by SPRECT_3:25;
then A15: (RightComp (Cage (C,n))) /\ (L~ (Cage (C,n))) = {} ;
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 object ; :: 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 object 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: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 object ; :: 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))) ` ) )
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:29; :: thesis: verum
end;
case A42: 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))) ) )
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: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;
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: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;
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: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;
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: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;
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: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;
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: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;
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: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;
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: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;
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;
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