let f be V8() standard special_circular_sequence; :: thesis: L~ f = (Cl (RightComp f)) \ (RightComp f)

thus L~ f c= (Cl (RightComp f)) \ (RightComp f) :: according to XBOOLE_0:def 10 :: thesis: (Cl (RightComp f)) \ (RightComp f) c= L~ f

then consider q being object such that

A26: q in (Cl (RightComp f)) \ (RightComp f) and

A27: not q in L~ f ;

reconsider q = q as Point of (TOP-REAL 2) by A26;

not q in RightComp f by A26, XBOOLE_0:def 5;

then A28: q in LeftComp f by A27, Th16;

q in Cl (RightComp f) by A26, XBOOLE_0:def 5;

then LeftComp f meets RightComp f by A28, PRE_TOPC:def 7;

hence contradiction by Th14; :: thesis: verum

thus L~ f c= (Cl (RightComp f)) \ (RightComp f) :: according to XBOOLE_0:def 10 :: thesis: (Cl (RightComp f)) \ (RightComp f) c= L~ f

proof

assume
not (Cl (RightComp f)) \ (RightComp f) c= L~ f
; :: thesis: contradiction
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in (Cl (RightComp f)) \ (RightComp f) )

assume A1: x in L~ f ; :: thesis: x in (Cl (RightComp f)) \ (RightComp f)

then reconsider p = x as Point of (TOP-REAL 2) ;

consider i being Nat such that

A2: ( 1 <= i & i + 1 <= len f ) and

A3: p in LSeg (f,i) by A1, SPPOL_2:13;

for O being Subset of (TOP-REAL 2) st O is open & p in O holds

RightComp f meets O

not x in RightComp f by A1, Th16;

hence x in (Cl (RightComp f)) \ (RightComp f) by A25, XBOOLE_0:def 5; :: thesis: verum

end;assume A1: x in L~ f ; :: thesis: x in (Cl (RightComp f)) \ (RightComp f)

then reconsider p = x as Point of (TOP-REAL 2) ;

consider i being Nat such that

A2: ( 1 <= i & i + 1 <= len f ) and

A3: p in LSeg (f,i) by A1, SPPOL_2:13;

for O being Subset of (TOP-REAL 2) st O is open & p in O holds

RightComp f meets O

proof

then A25:
p in Cl (RightComp f)
by PRE_TOPC:def 7;
(left_cell (f,i)) /\ (right_cell (f,i)) = LSeg (f,i)
by A2, GOBOARD5:31;

then LSeg (f,i) c= right_cell (f,i) by XBOOLE_1:17;

then A4: p in right_cell (f,i) by A3;

f is_sequence_on GoB f by GOBOARD5:def 5;

then consider i1, j1, i2, j2 being Nat such that

A5: [i1,j1] in Indices (GoB f) and

A6: f /. i = (GoB f) * (i1,j1) and

A7: [i2,j2] in Indices (GoB f) and

A8: f /. (i + 1) = (GoB f) * (i2,j2) and

A9: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A2, JORDAN8:3;

A10: 1 <= i1 by A5, MATRIX_0:32;

A11: j2 <= width (GoB f) by A7, MATRIX_0:32;

A12: 1 <= j1 by A5, MATRIX_0:32;

A13: j1 <= width (GoB f) by A5, MATRIX_0:32;

A14: i1 <= len (GoB f) by A5, MATRIX_0:32;

A15: i2 <= len (GoB f) by A7, MATRIX_0:32;

assume ( O is open & p in O ) ; :: thesis: RightComp f meets O

then O meets Int (right_cell (f,i)) by A16, PRE_TOPC:def 7;

hence RightComp f meets O by A2, GOBOARD9:25, XBOOLE_1:63; :: thesis: verum

end;then LSeg (f,i) c= right_cell (f,i) by XBOOLE_1:17;

then A4: p in right_cell (f,i) by A3;

f is_sequence_on GoB f by GOBOARD5:def 5;

then consider i1, j1, i2, j2 being Nat such that

A5: [i1,j1] in Indices (GoB f) and

A6: f /. i = (GoB f) * (i1,j1) and

A7: [i2,j2] in Indices (GoB f) and

A8: f /. (i + 1) = (GoB f) * (i2,j2) and

A9: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A2, JORDAN8:3;

A10: 1 <= i1 by A5, MATRIX_0:32;

A11: j2 <= width (GoB f) by A7, MATRIX_0:32;

A12: 1 <= j1 by A5, MATRIX_0:32;

A13: j1 <= width (GoB f) by A5, MATRIX_0:32;

A14: i1 <= len (GoB f) by A5, MATRIX_0:32;

A15: i2 <= len (GoB f) by A7, MATRIX_0:32;

A16: now :: thesis: ( ( i1 = i2 & j1 + 1 = j2 & p in Cl (Int (right_cell (f,i))) ) or ( i1 + 1 = i2 & j1 = j2 & p in Cl (Int (right_cell (f,i))) ) or ( i1 = i2 + 1 & j1 = j2 & p in Cl (Int (right_cell (f,i))) ) or ( i1 = i2 & j1 = j2 + 1 & p in Cl (Int (right_cell (f,i))) ) )end;

let O be Subset of (TOP-REAL 2); :: thesis: ( O is open & p in O implies RightComp f meets O )per cases
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A9;

end;

case A17:
( i1 = i2 & j1 + 1 = j2 )
; :: thesis: p in Cl (Int (right_cell (f,i)))

set w = i1 -' 1;

A18: (i1 -' 1) + 1 = i1 by A10, XREAL_1:235;

then right_cell (f,i) = cell ((GoB f),((i1 -' 1) + 1),j1) by A2, A5, A6, A7, A8, A17, GOBOARD5:27;

hence p in Cl (Int (right_cell (f,i))) by A4, A14, A13, A18, GOBRD11:35; :: thesis: verum

end;A18: (i1 -' 1) + 1 = i1 by A10, XREAL_1:235;

then right_cell (f,i) = cell ((GoB f),((i1 -' 1) + 1),j1) by A2, A5, A6, A7, A8, A17, GOBOARD5:27;

hence p in Cl (Int (right_cell (f,i))) by A4, A14, A13, A18, GOBRD11:35; :: thesis: verum

case A19:
( i1 + 1 = i2 & j1 = j2 )
; :: thesis: p in Cl (Int (right_cell (f,i)))

set w = j1 -' 1;

( j1 -' 1 <= (j1 -' 1) + 1 & (j1 -' 1) + 1 <= width (GoB f) ) by A12, A13, NAT_1:11, XREAL_1:235;

then A20: j1 -' 1 <= width (GoB f) by XXREAL_0:2;

(j1 -' 1) + 1 = j1 by A12, XREAL_1:235;

then right_cell (f,i) = cell ((GoB f),i1,(j1 -' 1)) by A2, A5, A6, A7, A8, A19, GOBOARD5:28;

hence p in Cl (Int (right_cell (f,i))) by A4, A14, A20, GOBRD11:35; :: thesis: verum

end;( j1 -' 1 <= (j1 -' 1) + 1 & (j1 -' 1) + 1 <= width (GoB f) ) by A12, A13, NAT_1:11, XREAL_1:235;

then A20: j1 -' 1 <= width (GoB f) by XXREAL_0:2;

(j1 -' 1) + 1 = j1 by A12, XREAL_1:235;

then right_cell (f,i) = cell ((GoB f),i1,(j1 -' 1)) by A2, A5, A6, A7, A8, A19, GOBOARD5:28;

hence p in Cl (Int (right_cell (f,i))) by A4, A14, A20, GOBRD11:35; :: thesis: verum

case A21:
( i1 = i2 + 1 & j1 = j2 )
; :: thesis: p in Cl (Int (right_cell (f,i)))

set w = j1 -' 1;

A22: (j1 -' 1) + 1 = j1 by A12, XREAL_1:235;

then right_cell (f,i) = cell ((GoB f),i2,((j1 -' 1) + 1)) by A2, A5, A6, A7, A8, A21, GOBOARD5:29;

hence p in Cl (Int (right_cell (f,i))) by A4, A13, A15, A22, GOBRD11:35; :: thesis: verum

end;A22: (j1 -' 1) + 1 = j1 by A12, XREAL_1:235;

then right_cell (f,i) = cell ((GoB f),i2,((j1 -' 1) + 1)) by A2, A5, A6, A7, A8, A21, GOBOARD5:29;

hence p in Cl (Int (right_cell (f,i))) by A4, A13, A15, A22, GOBRD11:35; :: thesis: verum

case A23:
( i1 = i2 & j1 = j2 + 1 )
; :: thesis: p in Cl (Int (right_cell (f,i)))

set z = i1 -' 1;

( i1 -' 1 <= (i1 -' 1) + 1 & (i1 -' 1) + 1 <= len (GoB f) ) by A10, A14, NAT_1:11, XREAL_1:235;

then A24: i1 -' 1 <= len (GoB f) by XXREAL_0:2;

(i1 -' 1) + 1 = i1 by A10, XREAL_1:235;

then right_cell (f,i) = cell ((GoB f),(i1 -' 1),j2) by A2, A5, A6, A7, A8, A23, GOBOARD5:30;

hence p in Cl (Int (right_cell (f,i))) by A4, A11, A24, GOBRD11:35; :: thesis: verum

end;( i1 -' 1 <= (i1 -' 1) + 1 & (i1 -' 1) + 1 <= len (GoB f) ) by A10, A14, NAT_1:11, XREAL_1:235;

then A24: i1 -' 1 <= len (GoB f) by XXREAL_0:2;

(i1 -' 1) + 1 = i1 by A10, XREAL_1:235;

then right_cell (f,i) = cell ((GoB f),(i1 -' 1),j2) by A2, A5, A6, A7, A8, A23, GOBOARD5:30;

hence p in Cl (Int (right_cell (f,i))) by A4, A11, A24, GOBRD11:35; :: thesis: verum

assume ( O is open & p in O ) ; :: thesis: RightComp f meets O

then O meets Int (right_cell (f,i)) by A16, PRE_TOPC:def 7;

hence RightComp f meets O by A2, GOBOARD9:25, XBOOLE_1:63; :: thesis: verum

not x in RightComp f by A1, Th16;

hence x in (Cl (RightComp f)) \ (RightComp f) by A25, XBOOLE_0:def 5; :: thesis: verum

then consider q being object such that

A26: q in (Cl (RightComp f)) \ (RightComp f) and

A27: not q in L~ f ;

reconsider q = q as Point of (TOP-REAL 2) by A26;

not q in RightComp f by A26, XBOOLE_0:def 5;

then A28: q in LeftComp f by A27, Th16;

q in Cl (RightComp f) by A26, XBOOLE_0:def 5;

then LeftComp f meets RightComp f by A28, PRE_TOPC:def 7;

hence contradiction by Th14; :: thesis: verum