let f be non constant standard special_circular_sequence; :: thesis:
let p1, p2, p be Point of (TOP-REAL 2); :: thesis:
assume A1: (L~ f) /\ (LSeg (p1,p2)) = {p} ; :: thesis:
let rl, rp be Point of (TOP-REAL 2); :: thesis:
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:
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:

assume A14: not rp in LSeg (p1,p2) ; :: thesis:

per cases 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:

hence ( p1 in RightComp f or p2 in RightComp f ) by A12, Th14; :: thesis:

end;

suppose ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rp in C & p2 in C ) ; :: thesis:

hence ( p1 in RightComp f or p2 in RightComp f ) by A12, Th14; :: thesis:

end;

end;

end;

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;

A16: now :: thesis:

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

per cases 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:

hence ( p1 in LeftComp f or p2 in LeftComp f ) by A15, Th14; :: thesis:

end;

suppose ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rl in C & p2 in C ) ; :: thesis:

hence ( p1 in LeftComp f or p2 in LeftComp f ) by A15, Th14; :: thesis:

end;

end;

end;

A18: now :: thesis:

assume that
A19: not rl in LSeg (p1,p2) and
A20: not rp in LSeg (p1,p2) ; :: thesis:

per cases by A16, A19;

suppose A21: p1 in LeftComp f ; :: thesis:

now :: thesis:

per cases by A13, A20;

suppose p1 in RightComp f ; :: thesis:

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:

end;

suppose p2 in RightComp f ; :: thesis:

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:

end;

end;

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

end;

suppose A22: p2 in LeftComp f ; :: thesis:

now :: thesis:

per cases by A13, A20;

suppose p1 in RightComp f ; :: thesis:

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:

end;

suppose p2 in RightComp f ; :: thesis:

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:

end;

end;

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

end;

end;

end;

A23: now :: thesis:

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

per cases 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:

hence ( p1 in RightComp f or p2 in RightComp f ) by A12, Th14; :: thesis:

end;

suppose ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rp in C & p2 in C ) ; :: thesis:

hence ( p1 in RightComp f or p2 in RightComp f ) by A12, Th14; :: thesis:

end;

end;

end;

A25: now :: thesis:

assume that
A26: not rl in LSeg (p1,p2) and
A27: rp in LSeg (p1,p2) ; :: thesis:

per cases by A16, A26;

suppose A28: p1 in LeftComp f ; :: thesis:

now :: thesis:

per cases by A23, A27;

suppose p1 in RightComp f ; :: thesis:

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:

end;

suppose p2 in RightComp f ; :: thesis:

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:

end;

end;

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

end;

suppose A29: p2 in LeftComp f ; :: thesis:

now :: thesis:

per cases by A23, A27;

suppose p1 in RightComp f ; :: thesis:

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:

end;

suppose p2 in RightComp f ; :: thesis:

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:

end;

end;

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

end;

end;

end;

A30: now :: thesis:

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

per cases 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:

hence ( p1 in LeftComp f or p2 in LeftComp f ) by A15, Th14; :: thesis:

end;

suppose ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ f) ` & rl in C & p2 in C ) ; :: thesis:

hence ( p1 in LeftComp f or p2 in LeftComp f ) by A15, Th14; :: thesis:

end;

end;

end;

A32: now :: thesis:

assume that
A33: rl in LSeg (p1,p2) and
A34: rp in LSeg (p1,p2) ; :: thesis:

per cases by A30, A33;

suppose A35: p1 in LeftComp f ; :: thesis:

now :: thesis:

per cases by A23, A34;

suppose p1 in RightComp f ; :: thesis:

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:

end;

suppose p2 in RightComp f ; :: thesis:

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:

end;

end;

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

end;

suppose A36: p2 in LeftComp f ; :: thesis:

now :: thesis:

per cases by A23, A34;

suppose p1 in RightComp f ; :: thesis:

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:

end;

suppose p2 in RightComp f ; :: thesis:

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:

end;

end;

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

end;

end;

end;

A37: now :: thesis:

assume that
A38: rl in LSeg (p1,p2) and
A39: not rp in LSeg (p1,p2) ; :: thesis:

per cases by A30, A38;

suppose A40: p1 in LeftComp f ; :: thesis:

now :: thesis:

per cases by A13, A39;

suppose p1 in RightComp f ; :: thesis:

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:

end;

suppose p2 in RightComp f ; :: thesis:

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:

end;

end;

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

end;

suppose A41: p2 in LeftComp f ; :: thesis:

now :: thesis:

per cases by A13, A39;

suppose p1 in RightComp f ; :: thesis:

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:

end;

suppose p2 in RightComp f ; :: thesis:

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:

end;

end;

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

end;

end;

end;

per cases ;

suppose A42: rl in LSeg (p1,p2) ; :: thesis:

now :: thesis:

per cases ;

suppose rp in LSeg (p1,p2) ; :: thesis:

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:

end;

suppose not rp in LSeg (p1,p2) ; :: thesis:

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:

end;

end;

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

end;

suppose A43: not rl in LSeg (p1,p2) ; :: thesis:

now :: thesis:

per cases ;

suppose rp in LSeg (p1,p2) ; :: thesis:

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:

end;

suppose not rp in LSeg (p1,p2) ; :: thesis:

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:

end;

end;

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

end;

end;