let f be non constant standard special_circular_sequence; :: thesis: (L~ f) ` <> {}
LSeg (((1 / 2) * (((GoB f) * 1,((width (GoB f)) -' 1)) + ((GoB f) * 1,(width (GoB f))))) - |[1,0 ]|),(((GoB f) * 1,(width (GoB f))) + |[(- 1),1]|) misses L~ f by GOBOARD8:33;
then LSeg (((1 / 2) * (((GoB f) * 1,((width (GoB f)) -' 1)) + ((GoB f) * 1,(width (GoB f))))) - |[1,0 ]|),(((GoB f) * 1,(width (GoB f))) + |[(- 1),1]|) c= (L~ f) ` by SUBSET_1:43;
hence (L~ f) ` <> {} ; :: thesis: verum