let p, p1, p2 be Point of (TOP-REAL 2); for f being non constant standard special_circular_sequence st (L~ f) /\ (LSeg p1,p2) = {p} holds
for r being Point of (TOP-REAL 2) st not r in LSeg p1,p2 & not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) ) & ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & ( r in right_cell f,i,(GoB f) or r in left_cell f,i,(GoB f) ) & p in LSeg f,i ) & not r in L~ f & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not r in C or not p1 in C ) ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C )
let f be non constant standard special_circular_sequence; ( (L~ f) /\ (LSeg p1,p2) = {p} implies for r being Point of (TOP-REAL 2) st not r in LSeg p1,p2 & not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) ) & ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & ( r in right_cell f,i,(GoB f) or r in left_cell f,i,(GoB f) ) & p in LSeg f,i ) & not r in L~ f & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not r in C or not p1 in C ) ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
assume
(L~ f) /\ (LSeg p1,p2) = {p}
; for r being Point of (TOP-REAL 2) st not r in LSeg p1,p2 & not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) ) & ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & ( r in right_cell f,i,(GoB f) or r in left_cell f,i,(GoB f) ) & p in LSeg f,i ) & not r in L~ f & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not r in C or not p1 in C ) ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C )
then A1:
p in (L~ f) /\ (LSeg p1,p2)
by TARSKI:def 1;
then A2:
p in LSeg p1,p2
by XBOOLE_0:def 4;
let r be Point of (TOP-REAL 2); ( not r in LSeg p1,p2 & not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) ) & ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & ( r in right_cell f,i,(GoB f) or r in left_cell f,i,(GoB f) ) & p in LSeg f,i ) & not r in L~ f & ( for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not r in C or not p1 in C ) ) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
assume that
A3:
not r in LSeg p1,p2
and
A4:
not p1 in L~ f
and
A5:
not p2 in L~ f
and
A6:
( ( p1 `1 = p2 `1 & p1 `1 = r `1 ) or ( p1 `2 = p2 `2 & p1 `2 = r `2 ) )
and
A7:
ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & ( r in right_cell f,i,(GoB f) or r in left_cell f,i,(GoB f) ) & p in LSeg f,i )
and
A8:
not r in L~ f
; ( ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )
consider i being Element of NAT such that
A9:
( 1 <= i & i + 1 <= len f )
and
A10:
( r in right_cell f,i,(GoB f) or r in left_cell f,i,(GoB f) )
and
A11:
p in LSeg f,i
by A7;
A12:
right_cell f,i,(GoB f) is convex
by A9, Th23;
A13:
f is_sequence_on GoB f
by GOBOARD5:def 5;
then A14:
(right_cell f,i,(GoB f)) \ (L~ f) c= RightComp f
by A9, JORDAN9:29;
A16:
LSeg f,i c= right_cell f,i,(GoB f)
by A13, A9, JORDAN1H:28;
A17:
now assume that A18:
p1 in LSeg r,
p
and A19:
r in right_cell f,
i,
(GoB f)
;
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C )
LSeg r,
p c= right_cell f,
i,
(GoB f)
by A11, A16, A12, A19, JORDAN1:def 1;
then
p1 in (right_cell f,i,(GoB f)) \ (L~ f)
by A4, A18, XBOOLE_0:def 5;
hence
ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ f) ` &
r in C &
p1 in C )
by A14, A15, A19, Th15;
verum end;
A20:
left_cell f,i,(GoB f) is convex
by A9, Th23;
A21:
(left_cell f,i,(GoB f)) \ (L~ f) c= LeftComp f
by A13, A9, JORDAN9:29;
A23:
LSeg f,i c= left_cell f,i,(GoB f)
by A13, A9, JORDAN1H:26;
A24:
now assume that A25:
p1 in LSeg r,
p
and A26:
r in left_cell f,
i,
(GoB f)
;
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p1 in C )
LSeg r,
p c= left_cell f,
i,
(GoB f)
by A11, A23, A20, A26, JORDAN1:def 1;
then
p1 in (left_cell f,i,(GoB f)) \ (L~ f)
by A4, A25, XBOOLE_0:def 5;
hence
ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ f) ` &
r in C &
p1 in C )
by A21, A22, A26, Th15;
verum end;
A27:
now assume that A28:
p2 in LSeg r,
p
and A29:
r in left_cell f,
i,
(GoB f)
;
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C )
LSeg r,
p c= left_cell f,
i,
(GoB f)
by A11, A23, A20, A29, JORDAN1:def 1;
then
p2 in (left_cell f,i,(GoB f)) \ (L~ f)
by A5, A28, XBOOLE_0:def 5;
hence
ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ f) ` &
r in C &
p2 in C )
by A21, A22, A29, Th15;
verum end;
A30:
now assume that A31:
p2 in LSeg r,
p
and A32:
r in right_cell f,
i,
(GoB f)
;
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & r in C & p2 in C )
LSeg r,
p c= right_cell f,
i,
(GoB f)
by A11, A16, A12, A32, JORDAN1:def 1;
then
p2 in (right_cell f,i,(GoB f)) \ (L~ f)
by A5, A31, XBOOLE_0:def 5;
hence
ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ f) ` &
r in C &
p2 in C )
by A14, A15, A32, Th15;
verum end;
A33:
( p <> p2 & p <> p1 )
by A4, A5, A1, XBOOLE_0:def 4;