let f be V8() standard special_circular_sequence; :: thesis: L~ f = (Cl ()) \ ()
thus L~ f c= (Cl ()) \ () :: according to XBOOLE_0:def 10 :: thesis: (Cl ()) \ () c= L~ f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in (Cl ()) \ () )
assume A1: x in L~ f ; :: thesis: x in (Cl ()) \ ()
then reconsider p = x as Point of () ;
consider i being Nat such that
A2: ( 1 <= i & i + 1 <= len f ) and
A3: p in LSeg (f,i) by ;
for O being Subset of () 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 ;
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 ;
A10: 1 <= i1 by ;
A11: j2 <= width (GoB f) by ;
A12: 1 <= j1 by ;
A13: j1 <= width (GoB f) by ;
A14: i1 <= len (GoB f) by ;
A15: i2 <= len (GoB f) by ;
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))) ) )
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;
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 ;
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 ; :: thesis: verum
end;
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 ;
then A20: j1 -' 1 <= width (GoB f) by XXREAL_0:2;
(j1 -' 1) + 1 = j1 by ;
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 ; :: thesis: verum
end;
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 ;
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 ; :: thesis: verum
end;
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 ;
then A24: i1 -' 1 <= len (GoB f) by XXREAL_0:2;
(i1 -' 1) + 1 = i1 by ;
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 ; :: thesis: verum
end;
end;
end;
let O be Subset of (); :: thesis: ( O is open & p in O implies RightComp f meets O )
assume ( O is open & p in O ) ; :: thesis:
then O meets Int (right_cell (f,i)) by ;
hence RightComp f meets O by ; :: thesis: verum
end;
then A25: p in Cl () by PRE_TOPC:def 7;
not x in RightComp f by ;
hence x in (Cl ()) \ () by ; :: thesis: verum
end;
assume not (Cl ()) \ () c= L~ f ; :: thesis: contradiction
then consider q being object such that
A26: q in (Cl ()) \ () and
A27: not q in L~ f ;
reconsider q = q as Point of () by A26;
not q in RightComp f by ;
then A28: q in LeftComp f by ;
q in Cl () by ;
then LeftComp f meets RightComp f by ;
hence contradiction by Th14; :: thesis: verum