let f be non constant standard special_circular_sequence; for p1, p2, p being Point of (TOP-REAL 2) st (L~ f) /\ (LSeg (p1,p2)) = {p} holds
for rl, rp being Point of (TOP-REAL 2) st not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = rl `1 & rl `1 = rp `1 ) or ( p1 `2 = p2 `2 & p1 `2 = rl `2 & rl `2 = rp `2 ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len f & rl in left_cell (f,i,(GoB f)) & rp in right_cell (f,i,(GoB f)) & p in LSeg (f,i) ) & not rl in L~ f & not rp in L~ f holds
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
let p1, p2, p be Point of (TOP-REAL 2); ( (L~ f) /\ (LSeg (p1,p2)) = {p} implies for rl, rp being Point of (TOP-REAL 2) st not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = rl `1 & rl `1 = rp `1 ) or ( p1 `2 = p2 `2 & p1 `2 = rl `2 & rl `2 = rp `2 ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len f & rl in left_cell (f,i,(GoB f)) & rp in right_cell (f,i,(GoB f)) & p in LSeg (f,i) ) & not rl in L~ f & not rp in L~ f holds
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) )
assume A1:
(L~ f) /\ (LSeg (p1,p2)) = {p}
; for rl, rp being Point of (TOP-REAL 2) st not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = rl `1 & rl `1 = rp `1 ) or ( p1 `2 = p2 `2 & p1 `2 = rl `2 & rl `2 = rp `2 ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len f & rl in left_cell (f,i,(GoB f)) & rp in right_cell (f,i,(GoB f)) & p in LSeg (f,i) ) & not rl in L~ f & not rp in L~ f holds
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
let rl, rp be Point of (TOP-REAL 2); ( not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = rl `1 & rl `1 = rp `1 ) or ( p1 `2 = p2 `2 & p1 `2 = rl `2 & rl `2 = rp `2 ) ) & ex i being Nat st
( 1 <= i & i + 1 <= len f & rl in left_cell (f,i,(GoB f)) & rp in right_cell (f,i,(GoB f)) & p in LSeg (f,i) ) & not rl in L~ f & not rp in L~ f implies for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) )
assume that
A2:
( not p1 in L~ f & not p2 in L~ f & ( ( p1 `1 = p2 `1 & p1 `1 = rl `1 & rl `1 = rp `1 ) or ( p1 `2 = p2 `2 & p1 `2 = rl `2 & rl `2 = rp `2 ) ) )
and
A3:
ex i being Nat st
( 1 <= i & i + 1 <= len f & rl in left_cell (f,i,(GoB f)) & rp in right_cell (f,i,(GoB f)) & p in LSeg (f,i) )
and
A4:
not rl in L~ f
and
A5:
not rp in L~ f
; for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
consider i being Nat such that
A6:
( 1 <= i & i + 1 <= len f )
and
A7:
rl in left_cell (f,i,(GoB f))
and
A8:
rp in right_cell (f,i,(GoB f))
by A3;
A9:
f is_sequence_on GoB f
by GOBOARD5:def 5;
then A10:
(left_cell (f,i,(GoB f))) \ (L~ f) c= LeftComp f
by A6, JORDAN9:27;
A11:
(right_cell (f,i,(GoB f))) \ (L~ f) c= RightComp f
by A9, A6, JORDAN9:27;
rp in (right_cell (f,i,(GoB f))) \ (L~ f)
by A5, A8, XBOOLE_0:def 5;
then A12:
not rp in LeftComp f
by A11, GOBRD14:18;
rl in (left_cell (f,i,(GoB f))) \ (L~ f)
by A4, A7, XBOOLE_0:def 5;
then A15:
not rl in RightComp f
by A10, GOBRD14:17;