let f be V8() standard special_circular_sequence; L~ f = (Cl (RightComp f)) \ (RightComp f)
thus
L~ f c= (Cl (RightComp f)) \ (RightComp f)
XBOOLE_0:def 10 (Cl (RightComp f)) \ (RightComp f) c= L~ fproof
let x be
object ;
TARSKI:def 3 ( not x in L~ f or x in (Cl (RightComp f)) \ (RightComp f) )
assume A1:
x in L~ f
;
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
(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 ( ( 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 )
;
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;
verum end; case A19:
(
i1 + 1
= i2 &
j1 = j2 )
;
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;
verum end; case A21:
(
i1 = i2 + 1 &
j1 = j2 )
;
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;
verum end; case A23:
(
i1 = i2 &
j1 = j2 + 1 )
;
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;
verum end; end; end;
let O be
Subset of
(TOP-REAL 2);
( O is open & p in O implies RightComp f meets O )
assume
(
O is
open &
p in O )
;
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;
verum
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;
verum
end;
assume
not (Cl (RightComp f)) \ (RightComp f) c= L~ f
; contradiction
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; verum