let f be non constant standard special_circular_sequence; :: thesis: 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); :: thesis: ( (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} ; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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;

then A15: not rl in RightComp f by A10, GOBRD14:17;

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); :: thesis: ( (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} ; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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;

A13: now :: thesis: ( rp in LSeg (p1,p2) or p1 in RightComp f or p2 in RightComp f )

rl in (left_cell (f,i,(GoB f))) \ (L~ f)
by A4, A7, XBOOLE_0:def 5;assume A14:
not rp in LSeg (p1,p2)
; :: thesis: ( p1 in RightComp f or p2 in RightComp f )

end;per cases
( ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rp in C & p2 in C ) ) by A1, A2, A3, A5, A14, Th30;

end;

( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rp in C & p2 in C ) ) by A1, A2, A3, A5, A14, Th30;

suppose
ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) ; :: thesis: ( p1 in RightComp f or p2 in RightComp f )

end;

( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) ; :: thesis: ( p1 in RightComp f or p2 in RightComp f )

end;

then A15: not rl in RightComp f by A10, GOBRD14:17;

A16: now :: thesis: ( rl in LSeg (p1,p2) or p1 in LeftComp f or p2 in LeftComp f )

assume A17:
not rl in LSeg (p1,p2)
; :: thesis: ( p1 in LeftComp f or p2 in LeftComp f )

end;per cases
( ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rl in C & p2 in C ) ) by A1, A2, A3, A4, A17, Th30;

end;

( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rl in C & p2 in C ) ) by A1, A2, A3, A4, A17, Th30;

suppose
ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) ; :: thesis: ( p1 in LeftComp f or p2 in LeftComp f )

end;

( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) ; :: thesis: ( p1 in LeftComp f or p2 in LeftComp f )

end;

A18: now :: thesis: ( not rl in LSeg (p1,p2) & not rp in LSeg (p1,p2) 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 ) )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) )

assume that

A19: not rl in LSeg (p1,p2) and

A20: not rp in LSeg (p1,p2) ; :: thesis: 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 )

end;A19: not rl in LSeg (p1,p2) and

A20: not rp in LSeg (p1,p2) ; :: thesis: 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 )

per cases
( p1 in LeftComp f or p2 in LeftComp f )
by A16, A19;

end;

suppose A21:
p1 in LeftComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

end;

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

now :: thesis: 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 )end;

hence
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 )

per cases
( p1 in RightComp f or p2 in RightComp f )
by A13, A20;

end;

suppose
p1 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

then
LeftComp f meets RightComp f
by A21, XBOOLE_0:3;

hence 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 ) by GOBRD14:14; :: thesis: verum

end;hence 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 ) by GOBRD14:14; :: thesis: verum

suppose
p2 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence
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 ) by A21, Th15; :: thesis: verum

end;( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by A21, Th15; :: thesis: verum

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

suppose A22:
p2 in LeftComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

end;

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

now :: thesis: 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 )end;

hence
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 )

per cases
( p1 in RightComp f or p2 in RightComp f )
by A13, A20;

end;

suppose
p1 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence
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 ) by A22, Th15; :: thesis: verum

end;( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by A22, Th15; :: thesis: verum

suppose
p2 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

then
LeftComp f meets RightComp f
by A22, XBOOLE_0:3;

hence 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 ) by GOBRD14:14; :: thesis: verum

end;hence 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 ) by GOBRD14:14; :: thesis: verum

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

A23: now :: thesis: ( not rp in LSeg (p1,p2) or p1 in RightComp f or p2 in RightComp f )

assume A24:
rp in LSeg (p1,p2)
; :: thesis: ( p1 in RightComp f or p2 in RightComp f )

end;per cases
( ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rp in C & p2 in C ) ) by A1, A5, A24, Lm5;

suppose
ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) ; :: thesis: ( p1 in RightComp f or p2 in RightComp f )

end;end;

( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rp in C & p2 in C ) ) by A1, A5, A24, Lm5;

( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) ; :: thesis: ( p1 in RightComp f or p2 in RightComp f )

end;

A25: now :: thesis: ( not rl in LSeg (p1,p2) & rp in LSeg (p1,p2) 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 ) )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) )

assume that

A26: not rl in LSeg (p1,p2) and

A27: rp in LSeg (p1,p2) ; :: thesis: 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 )

end;A26: not rl in LSeg (p1,p2) and

A27: rp in LSeg (p1,p2) ; :: thesis: 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 )

per cases
( p1 in LeftComp f or p2 in LeftComp f )
by A16, A26;

end;

suppose A28:
p1 in LeftComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

end;

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

now :: thesis: 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 )end;

hence
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 )

per cases
( p1 in RightComp f or p2 in RightComp f )
by A23, A27;

end;

suppose
p1 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

then
LeftComp f meets RightComp f
by A28, XBOOLE_0:3;

hence 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 ) by GOBRD14:14; :: thesis: verum

end;hence 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 ) by GOBRD14:14; :: thesis: verum

suppose
p2 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence
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 ) by A28, Th15; :: thesis: verum

end;( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by A28, Th15; :: thesis: verum

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

suppose A29:
p2 in LeftComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

end;

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

now :: thesis: 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 )end;

hence
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 )

per cases
( p1 in RightComp f or p2 in RightComp f )
by A23, A27;

end;

suppose
p1 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence
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 ) by A29, Th15; :: thesis: verum

end;( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by A29, Th15; :: thesis: verum

suppose
p2 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

then
LeftComp f meets RightComp f
by A29, XBOOLE_0:3;

hence 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 ) by GOBRD14:14; :: thesis: verum

end;hence 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 ) by GOBRD14:14; :: thesis: verum

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

A30: now :: thesis: ( not rl in LSeg (p1,p2) or p1 in LeftComp f or p2 in LeftComp f )

assume A31:
rl in LSeg (p1,p2)
; :: thesis: ( p1 in LeftComp f or p2 in LeftComp f )

end;per cases
( ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rl in C & p2 in C ) ) by A1, A4, A31, Lm5;

suppose
ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) ; :: thesis: ( p1 in LeftComp f or p2 in LeftComp f )

end;end;

( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) or ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & rl in C & p2 in C ) ) by A1, A4, A31, Lm5;

( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) ; :: thesis: ( p1 in LeftComp f or p2 in LeftComp f )

end;

A32: now :: thesis: ( rl in LSeg (p1,p2) & rp in LSeg (p1,p2) 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 ) )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) )

assume that

A33: rl in LSeg (p1,p2) and

A34: rp in LSeg (p1,p2) ; :: thesis: 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 )

end;A33: rl in LSeg (p1,p2) and

A34: rp in LSeg (p1,p2) ; :: thesis: 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 )

per cases
( p1 in LeftComp f or p2 in LeftComp f )
by A30, A33;

end;

suppose A35:
p1 in LeftComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

end;

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

now :: thesis: 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 )end;

hence
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 )

per cases
( p1 in RightComp f or p2 in RightComp f )
by A23, A34;

end;

suppose
p1 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

then
LeftComp f meets RightComp f
by A35, XBOOLE_0:3;

hence 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 ) by GOBRD14:14; :: thesis: verum

end;hence 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 ) by GOBRD14:14; :: thesis: verum

suppose
p2 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence
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 ) by A35, Th15; :: thesis: verum

end;( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by A35, Th15; :: thesis: verum

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

suppose A36:
p2 in LeftComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

end;

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

now :: thesis: 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 )end;

hence
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 )

per cases
( p1 in RightComp f or p2 in RightComp f )
by A23, A34;

end;

suppose
p1 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence
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 ) by A36, Th15; :: thesis: verum

end;( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by A36, Th15; :: thesis: verum

suppose
p2 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

then
LeftComp f meets RightComp f
by A36, XBOOLE_0:3;

hence 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 ) by GOBRD14:14; :: thesis: verum

end;hence 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 ) by GOBRD14:14; :: thesis: verum

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

A37: now :: thesis: ( rl in LSeg (p1,p2) & not rp in LSeg (p1,p2) 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 ) )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) )

assume that

A38: rl in LSeg (p1,p2) and

A39: not rp in LSeg (p1,p2) ; :: thesis: 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 )

end;A38: rl in LSeg (p1,p2) and

A39: not rp in LSeg (p1,p2) ; :: thesis: 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 )

per cases
( p1 in LeftComp f or p2 in LeftComp f )
by A30, A38;

end;

suppose A40:
p1 in LeftComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

end;

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

now :: thesis: 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 )end;

hence
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 )

per cases
( p1 in RightComp f or p2 in RightComp f )
by A13, A39;

end;

suppose
p1 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

then
LeftComp f meets RightComp f
by A40, XBOOLE_0:3;

hence 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 ) by GOBRD14:14; :: thesis: verum

end;hence 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 ) by GOBRD14:14; :: thesis: verum

suppose
p2 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence
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 ) by A40, Th15; :: thesis: verum

end;( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by A40, Th15; :: thesis: verum

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

suppose A41:
p2 in LeftComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

end;

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

now :: thesis: 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 )end;

hence
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 )

per cases
( p1 in RightComp f or p2 in RightComp f )
by A13, A39;

end;

suppose
p1 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence
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 ) by A41, Th15; :: thesis: verum

end;( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by A41, Th15; :: thesis: verum

suppose
p2 in RightComp f
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

then
LeftComp f meets RightComp f
by A41, XBOOLE_0:3;

hence 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 ) by GOBRD14:14; :: thesis: verum

end;hence 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 ) by GOBRD14:14; :: thesis: verum

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

per cases
( rl in LSeg (p1,p2) or not rl in LSeg (p1,p2) )
;

end;

suppose A42:
rl in LSeg (p1,p2)
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

end;

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

now :: thesis: 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 )end;

hence
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 )

per cases
( rp in LSeg (p1,p2) or not rp in LSeg (p1,p2) )
;

end;

suppose
rp in LSeg (p1,p2)
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence
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 ) by A32, A42; :: thesis: verum

end;( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by A32, A42; :: thesis: verum

suppose
not rp in LSeg (p1,p2)
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence
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 ) by A37, A42; :: thesis: verum

end;( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by A37, A42; :: thesis: verum

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

suppose A43:
not rl in LSeg (p1,p2)
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

end;

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

now :: thesis: 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 )end;

hence
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 )

per cases
( rp in LSeg (p1,p2) or not rp in LSeg (p1,p2) )
;

end;

suppose
rp in LSeg (p1,p2)
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence
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 ) by A25, A43; :: thesis: verum

end;( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by A25, A43; :: thesis: verum

suppose
not rp in LSeg (p1,p2)
; :: thesis: 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 )

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence
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 ) by A18, A43; :: thesis: verum

end;( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by A18, A43; :: thesis: verum

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum