let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: 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 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; :: thesis: ( (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 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} ; :: thesis: 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 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); :: thesis: ( 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 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 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 ; :: thesis: ( 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 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, Th22;

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:27;

A21: (left_cell (f,i,(GoB f))) \ (L~ f) c= LeftComp f by A13, A9, JORDAN9:27;

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

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:27;

A15: now :: thesis: ( r in right_cell (f,i,(GoB f)) implies r in RightComp f )

A16:
LSeg (f,i) c= right_cell (f,i,(GoB f))
by A13, A9, JORDAN1H:22;assume
r in right_cell (f,i,(GoB f))
; :: thesis: r in RightComp f

then r in (right_cell (f,i,(GoB f))) \ (L~ f) by A8, XBOOLE_0:def 5;

hence r in RightComp f by A14; :: thesis: verum

end;then r in (right_cell (f,i,(GoB f))) \ (L~ f) by A8, XBOOLE_0:def 5;

hence r in RightComp f by A14; :: thesis: verum

A17: now :: thesis: ( p1 in LSeg (r,p) & r in right_cell (f,i,(GoB f)) implies ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & r in C & p1 in C ) )

A20:
left_cell (f,i,(GoB f)) is convex
by A9, Th22;( C is_a_component_of (L~ f) ` & r in C & p1 in C ) )

assume that

A18: p1 in LSeg (r,p) and

A19: r in right_cell (f,i,(GoB f)) ; :: thesis: 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;

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, Th14; :: thesis: verum

end;A18: p1 in LSeg (r,p) and

A19: r in right_cell (f,i,(GoB f)) ; :: thesis: 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;

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, Th14; :: thesis: verum

A21: (left_cell (f,i,(GoB f))) \ (L~ f) c= LeftComp f by A13, A9, JORDAN9:27;

A22: now :: thesis: ( r in left_cell (f,i,(GoB f)) implies r in LeftComp f )

A23:
LSeg (f,i) c= left_cell (f,i,(GoB f))
by A13, A9, JORDAN1H:20;assume
r in left_cell (f,i,(GoB f))
; :: thesis: r in LeftComp f

then r in (left_cell (f,i,(GoB f))) \ (L~ f) by A8, XBOOLE_0:def 5;

hence r in LeftComp f by A21; :: thesis: verum

end;then r in (left_cell (f,i,(GoB f))) \ (L~ f) by A8, XBOOLE_0:def 5;

hence r in LeftComp f by A21; :: thesis: verum

A24: now :: thesis: ( p1 in LSeg (r,p) & r in left_cell (f,i,(GoB f)) implies ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & r in C & p1 in C ) )

( C is_a_component_of (L~ f) ` & r in C & p1 in C ) )

assume that

A25: p1 in LSeg (r,p) and

A26: r in left_cell (f,i,(GoB f)) ; :: thesis: 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;

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, Th14; :: thesis: verum

end;A25: p1 in LSeg (r,p) and

A26: r in left_cell (f,i,(GoB f)) ; :: thesis: 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;

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, Th14; :: thesis: verum

A27: now :: thesis: ( p2 in LSeg (r,p) & r in left_cell (f,i,(GoB f)) implies ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )

( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )

assume that

A28: p2 in LSeg (r,p) and

A29: r in left_cell (f,i,(GoB f)) ; :: thesis: 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;

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, Th14; :: thesis: verum

end;A28: p2 in LSeg (r,p) and

A29: r in left_cell (f,i,(GoB f)) ; :: thesis: 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;

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, Th14; :: thesis: verum

A30: now :: thesis: ( p2 in LSeg (r,p) & r in right_cell (f,i,(GoB f)) implies ex C being Subset of (TOP-REAL 2) st

( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )

A33:
( p <> p2 & p <> p1 )
by A4, A5, A1, XBOOLE_0:def 4;( C is_a_component_of (L~ f) ` & r in C & p2 in C ) )

assume that

A31: p2 in LSeg (r,p) and

A32: r in right_cell (f,i,(GoB f)) ; :: thesis: 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;

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, Th14; :: thesis: verum

end;A31: p2 in LSeg (r,p) and

A32: r in right_cell (f,i,(GoB f)) ; :: thesis: 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;

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, Th14; :: thesis: verum

per cases
( p1 in LSeg (r,p) or p2 in LSeg (r,p) )
by A3, A6, A33, A2, Th28;

end;

suppose A34:
p1 in LSeg (r,p)
; :: thesis: ( 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 ) )

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

end;

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

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

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

per cases
( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) )
by A10;

end;

suppose
r in right_cell (f,i,(GoB f))
; :: thesis: ( 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 ) )

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

hence
( 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 ) ) by A17, A34; :: thesis: verum

end;( 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 ) ) by A17, A34; :: thesis: verum

suppose
r in left_cell (f,i,(GoB f))
; :: thesis: ( 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 ) )

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

hence
( 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 ) ) by A24, A34; :: thesis: verum

end;( 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 ) ) by A24, A34; :: thesis: verum

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

suppose A35:
p2 in LSeg (r,p)
; :: thesis: ( 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 ) )

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

end;

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

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

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

per cases
( r in right_cell (f,i,(GoB f)) or r in left_cell (f,i,(GoB f)) )
by A10;

end;

suppose
r in right_cell (f,i,(GoB f))
; :: thesis: ( 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 ) )

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

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

end;( 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 ) ) by A30, A35; :: thesis: verum

suppose
r in left_cell (f,i,(GoB f))
; :: thesis: ( 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 ) )

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

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

end;( 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 ) ) by A27, A35; :: thesis: verum

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