let f be non constant standard special_circular_sequence; :: thesis: for p1, p2, p being Point of () st (L~ f) /\ (LSeg (p1,p2)) = {p} holds
for rl, rp being Point of () 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 () 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 (); :: thesis: ( (L~ f) /\ (LSeg (p1,p2)) = {p} implies for rl, rp being Point of () 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 () 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 () 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 () 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 (); :: 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 () 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 () 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 ;
A11: (right_cell (f,i,(GoB f))) \ (L~ f) c= RightComp f by ;
rp in (right_cell (f,i,(GoB f))) \ (L~ f) by ;
then A12: not rp in LeftComp f by ;
A13: now :: thesis: ( rp in LSeg (p1,p2) or p1 in RightComp f or p2 in RightComp f )
assume A14: not rp in LSeg (p1,p2) ; :: thesis: ( p1 in RightComp f or p2 in RightComp f )
per cases ( ex C being Subset of () st
( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) or ex C being Subset of () 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 () st
( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) ; :: thesis: ( p1 in RightComp f or p2 in RightComp f )
hence ( p1 in RightComp f or p2 in RightComp f ) by ; :: thesis: verum
end;
suppose ex C being Subset of () st
( C is_a_component_of (L~ f) ` & rp in C & p2 in C ) ; :: thesis: ( p1 in RightComp f or p2 in RightComp f )
hence ( p1 in RightComp f or p2 in RightComp f ) by ; :: thesis: verum
end;
end;
end;
rl in (left_cell (f,i,(GoB f))) \ (L~ f) by ;
then A15: not rl in RightComp f by ;
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 )
per cases ( ex C being Subset of () st
( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) or ex C being Subset of () 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 () st
( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) ; :: thesis: ( p1 in LeftComp f or p2 in LeftComp f )
hence ( p1 in LeftComp f or p2 in LeftComp f ) by ; :: thesis: verum
end;
suppose ex C being Subset of () st
( C is_a_component_of (L~ f) ` & rl in C & p2 in C ) ; :: thesis: ( p1 in LeftComp f or p2 in LeftComp f )
hence ( p1 in LeftComp f or p2 in LeftComp f ) by ; :: thesis: verum
end;
end;
end;
A18: now :: thesis: ( not rl in LSeg (p1,p2) & not rp in LSeg (p1,p2) implies for C being Subset of () holds
( 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 () 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 ;
suppose A21: p1 in LeftComp f ; :: thesis: for C being Subset of () holds
( 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 () 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 ;
suppose p1 in RightComp f ; :: thesis: for C being Subset of () holds
( 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 ;
hence for C being Subset of () 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;
suppose p2 in RightComp f ; :: thesis: for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by ; :: thesis: verum
end;
end;
end;
hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum
end;
suppose A22: p2 in LeftComp f ; :: thesis: for C being Subset of () holds
( 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 () 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 ;
suppose p1 in RightComp f ; :: thesis: for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by ; :: thesis: verum
end;
suppose p2 in RightComp f ; :: thesis: for C being Subset of () holds
( 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 ;
hence for C being Subset of () 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;
end;
end;
hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum
end;
end;
end;
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 )
per cases ( ex C being Subset of () st
( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) or ex C being Subset of () 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 () st
( C is_a_component_of (L~ f) ` & rp in C & p1 in C ) ; :: thesis: ( p1 in RightComp f or p2 in RightComp f )
hence ( p1 in RightComp f or p2 in RightComp f ) by ; :: thesis: verum
end;
suppose ex C being Subset of () st
( C is_a_component_of (L~ f) ` & rp in C & p2 in C ) ; :: thesis: ( p1 in RightComp f or p2 in RightComp f )
hence ( p1 in RightComp f or p2 in RightComp f ) by ; :: thesis: verum
end;
end;
end;
A25: now :: thesis: ( not rl in LSeg (p1,p2) & rp in LSeg (p1,p2) implies for C being Subset of () holds
( 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 () 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 ;
suppose A28: p1 in LeftComp f ; :: thesis: for C being Subset of () holds
( 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 () 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 ;
suppose p1 in RightComp f ; :: thesis: for C being Subset of () holds
( 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 ;
hence for C being Subset of () 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;
suppose p2 in RightComp f ; :: thesis: for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by ; :: thesis: verum
end;
end;
end;
hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum
end;
suppose A29: p2 in LeftComp f ; :: thesis: for C being Subset of () holds
( 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 () 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 ;
suppose p1 in RightComp f ; :: thesis: for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by ; :: thesis: verum
end;
suppose p2 in RightComp f ; :: thesis: for C being Subset of () holds
( 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 ;
hence for C being Subset of () 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;
end;
end;
hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum
end;
end;
end;
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 )
per cases ( ex C being Subset of () st
( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) or ex C being Subset of () 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 () st
( C is_a_component_of (L~ f) ` & rl in C & p1 in C ) ; :: thesis: ( p1 in LeftComp f or p2 in LeftComp f )
hence ( p1 in LeftComp f or p2 in LeftComp f ) by ; :: thesis: verum
end;
suppose ex C being Subset of () st
( C is_a_component_of (L~ f) ` & rl in C & p2 in C ) ; :: thesis: ( p1 in LeftComp f or p2 in LeftComp f )
hence ( p1 in LeftComp f or p2 in LeftComp f ) by ; :: thesis: verum
end;
end;
end;
A32: now :: thesis: ( rl in LSeg (p1,p2) & rp in LSeg (p1,p2) implies for C being Subset of () holds
( 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 () 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 ;
suppose A35: p1 in LeftComp f ; :: thesis: for C being Subset of () holds
( 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 () 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 ;
suppose p1 in RightComp f ; :: thesis: for C being Subset of () holds
( 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 ;
hence for C being Subset of () 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;
suppose p2 in RightComp f ; :: thesis: for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by ; :: thesis: verum
end;
end;
end;
hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum
end;
suppose A36: p2 in LeftComp f ; :: thesis: for C being Subset of () holds
( 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 () 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 ;
suppose p1 in RightComp f ; :: thesis: for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by ; :: thesis: verum
end;
suppose p2 in RightComp f ; :: thesis: for C being Subset of () holds
( 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 ;
hence for C being Subset of () 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;
end;
end;
hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum
end;
end;
end;
A37: now :: thesis: ( rl in LSeg (p1,p2) & not rp in LSeg (p1,p2) implies for C being Subset of () holds
( 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 () 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 ;
suppose A40: p1 in LeftComp f ; :: thesis: for C being Subset of () holds
( 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 () 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 ;
suppose p1 in RightComp f ; :: thesis: for C being Subset of () holds
( 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 ;
hence for C being Subset of () 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;
suppose p2 in RightComp f ; :: thesis: for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by ; :: thesis: verum
end;
end;
end;
hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum
end;
suppose A41: p2 in LeftComp f ; :: thesis: for C being Subset of () holds
( 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 () 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 ;
suppose p1 in RightComp f ; :: thesis: for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by ; :: thesis: verum
end;
suppose p2 in RightComp f ; :: thesis: for C being Subset of () holds
( 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 ;
hence for C being Subset of () 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;
end;
end;
hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum
end;
end;
end;
per cases ( rl in LSeg (p1,p2) or not rl in LSeg (p1,p2) ) ;
suppose A42: rl in LSeg (p1,p2) ; :: thesis: for C being Subset of () holds
( 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 () 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) ) ;
suppose rp in LSeg (p1,p2) ; :: thesis: for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by ; :: thesis: verum
end;
suppose not rp in LSeg (p1,p2) ; :: thesis: for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by ; :: thesis: verum
end;
end;
end;
hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum
end;
suppose A43: not rl in LSeg (p1,p2) ; :: thesis: for C being Subset of () holds
( 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 () 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) ) ;
suppose rp in LSeg (p1,p2) ; :: thesis: for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by ; :: thesis: verum
end;
suppose not rp in LSeg (p1,p2) ; :: thesis: for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )

hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) by ; :: thesis: verum
end;
end;
end;
hence for C being Subset of () holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum
end;
end;