let n be Nat; 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); 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 ;
TARSKI:def 3 ( 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)))
;
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 A21:
not
q in L~ (Cage (C,n))
;
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 ;
TARSKI:def 3 ( not a in LSeg (p,s) or a in (L~ (Cage (C,n))) ` )
assume A38:
a in LSeg (
p,
s)
;
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 ( ( 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 A42:
b <> s
;
a in (L~ (Cage (C,n))) ` now ( ( 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 )
;
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;
verum end; case A47:
(
s `1 < p `1 &
s `2 > p `2 )
;
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;
verum end; case A51:
(
s `1 < p `1 &
s `2 = p `2 )
;
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;
verum end; case A54:
(
s `1 > p `1 &
s `2 < p `2 )
;
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;
verum end; case A58:
(
s `1 > p `1 &
s `2 > p `2 )
;
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;
verum end; case A62:
(
s `1 > p `1 &
s `2 = p `2 )
;
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;
verum end; case A65:
(
s `1 = p `1 &
s `2 > p `2 )
;
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;
verum end; case A68:
(
s `1 = p `1 &
s `2 < p `2 )
;
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;
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;
verum end; end; end;
hence
a in (L~ (Cage (C,n))) `
;
verum
end; A71:
s in LSeg (
p,
s)
by RLTOPSP1:68;
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;
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; verum