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;
A1: N-min C in C by SPRECT_1:13;
C misses L~ (Cage C,n) by Th5;
then C /\ (L~ (Cage C,n)) = {} by XBOOLE_0:def 7;
then A2: not N-min C in L~ (Cage C,n) by A1, XBOOLE_0:def 4;
RightComp (Cage C,n) misses L~ (Cage C,n) by SPRECT_3:42;
then A3: (RightComp (Cage C,n)) /\ (L~ (Cage C,n)) = {} by XBOOLE_0:def 7;
consider k being Element of NAT such that
A4: ( 1 <= k & k + 1 <= len (Gauge C,n) ) and
A5: (Cage C,n) /. 1 = (Gauge C,n) * k,(width (Gauge C,n)) and
A6: (Cage C,n) /. 2 = (Gauge C,n) * (k + 1),(width (Gauge C,n)) and
A7: 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;
A8: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
L~ (Cage C,n) <> {} ;
then A9: 1 + 1 <= len (Cage C,n) by GOBRD14:8;
A10: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A11: 1 <= k + 1 by NAT_1:11;
then A12: 1 <= len (Gauge C,n) by A4, XXREAL_0:2;
A13: k < len (Gauge C,n) by A4, NAT_1:13;
then ( [k,(len (Gauge C,n))] in Indices (Gauge C,n) & [(k + 1),(len (Gauge C,n))] in Indices (Gauge C,n) ) by A4, A10, A11, A12, MATRIX_1:37;
then A14: cell (Gauge C,n),k,((len (Gauge C,n)) -' 1) = right_cell (Cage C,n),1,(Gauge C,n) by A5, A6, A8, A9, A10, GOBRD13:25;
right_cell (Cage C,n),1,(Gauge C,n) c= right_cell (Cage C,n),1 by A8, A9, GOBRD13:34;
then A15: Int (right_cell (Cage C,n),1,(Gauge C,n)) c= Int (right_cell (Cage C,n),1) by TOPS_1:48;
Int (right_cell (Cage C,n),1) c= RightComp (Cage C,n) by GOBOARD9:def 2;
then A16: Int (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1)) c= RightComp (Cage C,n) by A14, A15, XBOOLE_1:1;
RightComp (Cage C,n) c= (RightComp (Cage C,n)) \/ (L~ (Cage C,n)) by XBOOLE_1:7;
then A17: Int (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1)) c= (RightComp (Cage C,n)) \/ (L~ (Cage C,n)) by A16, XBOOLE_1:1;
A18: right_cell (Cage C,n),1,(Gauge C,n) is closed by A8, A9, GOBRD13:31;
A19: 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 A20: 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 A21: (len (Gauge C,n)) -' 1 = (len (Gauge C,n)) - 1 by XREAL_0:def 2;
A22: (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 A10, A13, A21, GOBOARD9:17;
then consider p being set such that
A23: 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 A23;

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 A24: not q in L~ (Cage C,n) ; :: thesis: q in (RightComp (Cage C,n)) \/ (L~ (Cage C,n))

A25: LSeg p,s c= (L~ (Cage C,n)) `

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in LSeg p,s or a in (L~ (Cage C,n)) ` )
assume A26: a in LSeg p,s ; :: thesis: a in (L~ (Cage C,n)) `
then reconsider b = a as Point of (TOP-REAL 2) ;
3 <= (len (Gauge C,n)) -' 1 by GOBRD14:17;
then A27: 1 <= (len (Gauge C,n)) -' 1 by XXREAL_0:2;
then A28: 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 A4, A10, A13, A21, A22, GOBOARD6:29;
A29: b = |[(b `1 ),(b `2 )]| by EUCLID:57;
consider x, y being Real such that
A30: p = |[x,y]| and
A31: ( ((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 A23, A28;
Fr (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1)) c= cell (Gauge C,n),k,((len (Gauge C,n)) -' 1) by A8, A9, A14, GOBRD13:31, TOPS_1:69;
then A32: q in cell (Gauge C,n),k,((len (Gauge C,n)) -' 1) by A20;
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 A4, A10, A13, A21, A22, A27, GOBRD11:32;
then consider m, o being Real such that
A33: s = |[m,o]| and
A34: ( ((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 A32;
A35: ( s `1 = m & s `2 = o & p `1 = x & p `2 = y ) by A30, A33, 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 A24, SUBSET_1:50; :: thesis: verum

end;

case A36: 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 ( s `1 < p `1 & s `2 < p `2 ) ; :: thesis: b in Int (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1))

then ( s `1 < b `1 & b `1 <= p `1 & s `2 < b `2 & b `2 <= p `2 ) by A26, A36, TOPREAL6:37, TOPREAL6:38;
then ( ((Gauge C,n) * k,1) `1 < b `1 & b `1 < ((Gauge C,n) * (k + 1),1) `1 & ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 < b `2 & b `2 < ((Gauge C,n) * 1,(((len (Gauge C,n)) -' 1) + 1)) `2 ) by A31, A34, A35, XXREAL_0:2;
hence b in Int (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1)) by A28, A29; :: 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 ( s `1 < b `1 & b `1 <= p `1 & p `2 <= b `2 & b `2 < s `2 ) by A26, A36, TOPREAL6:37, TOPREAL6:38;
then ( ((Gauge C,n) * k,1) `1 < b `1 & b `1 < ((Gauge C,n) * (k + 1),1) `1 & ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 < b `2 & b `2 < ((Gauge C,n) * 1,(((len (Gauge C,n)) -' 1) + 1)) `2 ) by A31, A34, A35, XXREAL_0:2;
hence b in Int (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1)) by A28, A29; :: 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 ( s `1 < b `1 & b `1 <= p `1 & p `2 = b `2 & b `2 = s `2 ) by A26, A36, GOBOARD7:6, TOPREAL6:37;
then ( ((Gauge C,n) * k,1) `1 < b `1 & b `1 < ((Gauge C,n) * (k + 1),1) `1 & ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 < b `2 & b `2 < ((Gauge C,n) * 1,(((len (Gauge C,n)) -' 1) + 1)) `2 ) by A31, A34, A35, XXREAL_0:2;
hence b in Int (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1)) by A28, A29; :: 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 ( s `1 > b `1 & b `1 >= p `1 & s `2 < b `2 & b `2 <= p `2 ) by A26, A36, TOPREAL6:37, TOPREAL6:38;
then ( ((Gauge C,n) * k,1) `1 < b `1 & b `1 < ((Gauge C,n) * (k + 1),1) `1 & ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 < b `2 & b `2 < ((Gauge C,n) * 1,(((len (Gauge C,n)) -' 1) + 1)) `2 ) by A31, A34, A35, XXREAL_0:2;
hence b in Int (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1)) by A28, A29; :: 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 ( s `1 > b `1 & b `1 >= p `1 & s `2 > b `2 & b `2 >= p `2 ) by A26, A36, TOPREAL6:37, TOPREAL6:38;
then ( ((Gauge C,n) * k,1) `1 < b `1 & b `1 < ((Gauge C,n) * (k + 1),1) `1 & ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 < b `2 & b `2 < ((Gauge C,n) * 1,(((len (Gauge C,n)) -' 1) + 1)) `2 ) by A31, A34, A35, XXREAL_0:2;
hence b in Int (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1)) by A28, A29; :: 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 ( s `1 > b `1 & b `1 >= p `1 & s `2 = b `2 & b `2 = p `2 ) by A26, A36, GOBOARD7:6, TOPREAL6:37;
then ( ((Gauge C,n) * k,1) `1 < b `1 & b `1 < ((Gauge C,n) * (k + 1),1) `1 & ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 < b `2 & b `2 < ((Gauge C,n) * 1,(((len (Gauge C,n)) -' 1) + 1)) `2 ) by A31, A34, A35, XXREAL_0:2;
hence b in Int (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1)) by A28, A29; :: 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 ( s `1 = b `1 & b `1 = p `1 & s `2 > b `2 & b `2 >= p `2 ) by A26, A36, GOBOARD7:5, TOPREAL6:38;
then ( ((Gauge C,n) * k,1) `1 < b `1 & b `1 < ((Gauge C,n) * (k + 1),1) `1 & ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 < b `2 & b `2 < ((Gauge C,n) * 1,(((len (Gauge C,n)) -' 1) + 1)) `2 ) by A31, A34, A35, XXREAL_0:2;
hence b in Int (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1)) by A28, A29; :: 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 ( s `1 = b `1 & b `1 = p `1 & s `2 < b `2 & b `2 <= p `2 ) by A26, A36, GOBOARD7:5, TOPREAL6:38;
then ( ((Gauge C,n) * k,1) `1 < b `1 & b `1 < ((Gauge C,n) * (k + 1),1) `1 & ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 < b `2 & b `2 < ((Gauge C,n) * 1,(((len (Gauge C,n)) -' 1) + 1)) `2 ) by A31, A34, A35, XXREAL_0:2;
hence b in Int (cell (Gauge C,n),k,((len (Gauge C,n)) -' 1)) by A28, A29; :: 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 A23, A26, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then not b in L~ (Cage C,n) by A3, A16, 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;

A37: RightComp (Cage C,n) is_a_component_of (L~ (Cage C,n)) ` by GOBOARD9:def 2;
A38: {p} c= RightComp (Cage C,n) by A16, A23, ZFMISC_1:37;
{p} meets LSeg p,s

proof

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;

hence {p} meets LSeg p,s by XBOOLE_0:3; :: thesis: verum

end;

then A39: LSeg p,s c= RightComp (Cage C,n) by A25, A37, A38, GOBOARD9:6;
s in LSeg p,s by RLTOPSP1:69;
hence q in (RightComp (Cage C,n)) \/ (L~ (Cage C,n)) by A39, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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 A18, TOPS_1:77;
then (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;
then right_cell (Cage C,n),1,(Gauge C,n) c= (RightComp (Cage C,n)) \/ (L~ (Cage C,n)) by A14, A17, A19, XBOOLE_1:8;
hence N-min C in RightComp (Cage C,n) by A2, A7, A10, A14, XBOOLE_0:def 3; :: thesis: verum