let p1, p2 be Point of (TOP-REAL 2); :: thesis: for f being non constant standard special_circular_sequence

for r being Point of (TOP-REAL 2) st r in LSeg (p1,p2) & ex x being set st (L~ f) /\ (LSeg (p1,p2)) = {x} & not r in L~ f & not L~ f misses LSeg (p1,r) holds

L~ f misses LSeg (r,p2)

let f be non constant standard special_circular_sequence; :: thesis: for r being Point of (TOP-REAL 2) st r in LSeg (p1,p2) & ex x being set st (L~ f) /\ (LSeg (p1,p2)) = {x} & not r in L~ f & not L~ f misses LSeg (p1,r) holds

L~ f misses LSeg (r,p2)

let r be Point of (TOP-REAL 2); :: thesis: ( r in LSeg (p1,p2) & ex x being set st (L~ f) /\ (LSeg (p1,p2)) = {x} & not r in L~ f & not L~ f misses LSeg (p1,r) implies L~ f misses LSeg (r,p2) )

assume that

A1: r in LSeg (p1,p2) and

A2: ex x being set st (L~ f) /\ (LSeg (p1,p2)) = {x} and

A3: not r in L~ f ; :: thesis: ( L~ f misses LSeg (p1,r) or L~ f misses LSeg (r,p2) )

consider p being set such that

A4: (L~ f) /\ (LSeg (p1,p2)) = {p} by A2;

A5: p in {p} by TARSKI:def 1;

then A6: p in LSeg (p1,p2) by A4, XBOOLE_0:def 4;

reconsider p = p as Point of (TOP-REAL 2) by A4, A5;

then A9: LSeg (p2,r) c= LSeg (p1,p2) by A1, TOPREAL1:6;

p1 in LSeg (p1,p2) by RLTOPSP1:68;

then A10: LSeg (p1,r) c= LSeg (p1,p2) by A1, TOPREAL1:6;

for r being Point of (TOP-REAL 2) st r in LSeg (p1,p2) & ex x being set st (L~ f) /\ (LSeg (p1,p2)) = {x} & not r in L~ f & not L~ f misses LSeg (p1,r) holds

L~ f misses LSeg (r,p2)

let f be non constant standard special_circular_sequence; :: thesis: for r being Point of (TOP-REAL 2) st r in LSeg (p1,p2) & ex x being set st (L~ f) /\ (LSeg (p1,p2)) = {x} & not r in L~ f & not L~ f misses LSeg (p1,r) holds

L~ f misses LSeg (r,p2)

let r be Point of (TOP-REAL 2); :: thesis: ( r in LSeg (p1,p2) & ex x being set st (L~ f) /\ (LSeg (p1,p2)) = {x} & not r in L~ f & not L~ f misses LSeg (p1,r) implies L~ f misses LSeg (r,p2) )

assume that

A1: r in LSeg (p1,p2) and

A2: ex x being set st (L~ f) /\ (LSeg (p1,p2)) = {x} and

A3: not r in L~ f ; :: thesis: ( L~ f misses LSeg (p1,r) or L~ f misses LSeg (r,p2) )

consider p being set such that

A4: (L~ f) /\ (LSeg (p1,p2)) = {p} by A2;

A5: p in {p} by TARSKI:def 1;

then A6: p in LSeg (p1,p2) by A4, XBOOLE_0:def 4;

reconsider p = p as Point of (TOP-REAL 2) by A4, A5;

A7: now :: thesis: ( (LSeg (p1,r)) /\ (LSeg (r,p)) = {r} or (LSeg (p,r)) /\ (LSeg (r,p2)) = {r} )

p2 in LSeg (p1,p2)
by RLTOPSP1:68;A8:
LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2))
by A6, TOPREAL1:5;

end;per cases
( r in LSeg (p1,p) or r in LSeg (p,p2) )
by A1, A8, XBOOLE_0:def 3;

end;

then A9: LSeg (p2,r) c= LSeg (p1,p2) by A1, TOPREAL1:6;

p1 in LSeg (p1,p2) by RLTOPSP1:68;

then A10: LSeg (p1,r) c= LSeg (p1,p2) by A1, TOPREAL1:6;

now :: thesis: ( L~ f meets LSeg (p1,r) implies not L~ f meets LSeg (r,p2) )

hence
( L~ f misses LSeg (p1,r) or L~ f misses LSeg (r,p2) )
; :: thesis: verumassume that

A11: L~ f meets LSeg (p1,r) and

A12: L~ f meets LSeg (r,p2) ; :: thesis: contradiction

end;A11: L~ f meets LSeg (p1,r) and

A12: L~ f meets LSeg (r,p2) ; :: thesis: contradiction

per cases
( (LSeg (p1,r)) /\ (LSeg (r,p)) = {r} or (LSeg (p,r)) /\ (LSeg (r,p2)) = {r} )
by A7;

end;

suppose A13:
(LSeg (p1,r)) /\ (LSeg (r,p)) = {r}
; :: thesis: contradiction

consider x being object such that

A14: x in L~ f and

A15: x in LSeg (p1,r) by A11, XBOOLE_0:3;

x in (L~ f) /\ (LSeg (p1,p2)) by A10, A14, A15, XBOOLE_0:def 4;

then x = p by A4, TARSKI:def 1;

then x in LSeg (r,p) by RLTOPSP1:68;

then x in (LSeg (p1,r)) /\ (LSeg (r,p)) by A15, XBOOLE_0:def 4;

hence contradiction by A3, A13, A14, TARSKI:def 1; :: thesis: verum

end;A14: x in L~ f and

A15: x in LSeg (p1,r) by A11, XBOOLE_0:3;

x in (L~ f) /\ (LSeg (p1,p2)) by A10, A14, A15, XBOOLE_0:def 4;

then x = p by A4, TARSKI:def 1;

then x in LSeg (r,p) by RLTOPSP1:68;

then x in (LSeg (p1,r)) /\ (LSeg (r,p)) by A15, XBOOLE_0:def 4;

hence contradiction by A3, A13, A14, TARSKI:def 1; :: thesis: verum

suppose A16:
(LSeg (p,r)) /\ (LSeg (r,p2)) = {r}
; :: thesis: contradiction

consider x being object such that

A17: x in L~ f and

A18: x in LSeg (r,p2) by A12, XBOOLE_0:3;

x in (L~ f) /\ (LSeg (p1,p2)) by A9, A17, A18, XBOOLE_0:def 4;

then x = p by A4, TARSKI:def 1;

then x in LSeg (p,r) by RLTOPSP1:68;

then x in (LSeg (p,r)) /\ (LSeg (r,p2)) by A18, XBOOLE_0:def 4;

hence contradiction by A3, A16, A17, TARSKI:def 1; :: thesis: verum

end;A17: x in L~ f and

A18: x in LSeg (r,p2) by A12, XBOOLE_0:3;

x in (L~ f) /\ (LSeg (p1,p2)) by A9, A17, A18, XBOOLE_0:def 4;

then x = p by A4, TARSKI:def 1;

then x in LSeg (p,r) by RLTOPSP1:68;

then x in (LSeg (p,r)) /\ (LSeg (r,p2)) by A18, XBOOLE_0:def 4;

hence contradiction by A3, A16, A17, TARSKI:def 1; :: thesis: verum