let f be constant standard special_circular_sequence; :: thesis:
thus L~ f c= (Cl (RightComp f)) \ (RightComp f) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in L~ f ; :: thesis:
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

(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;

A16: now :: thesis:

per cases by A9;

case A17: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

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:

end;

case A19: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

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:

end;

case A21: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

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:

end;

case A23: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

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:

end;

end;

end;

let O be Subset of (TOP-REAL 2); :: thesis:
assume ( O is open & p in O ) ; :: thesis:
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:

end;

then A25: p in Cl (RightComp f) by PRE_TOPC:def 7;
not x in RightComp f by A1, Th16;
hence x in (Cl (RightComp f)) \ (RightComp f) by A25, XBOOLE_0:def 5; :: thesis:

end;

assume not (Cl (RightComp f)) \ (RightComp f) c= L~ f ; :: thesis:
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: