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;
p1 in LSeg p1,p2 by RLTOPSP1:69;
then A7: LSeg p1,r c= LSeg p1,p2 by A1, TOPREAL1:12;
p2 in LSeg p1,p2 by RLTOPSP1:69;
then A8: LSeg p2,r c= LSeg p1,p2 by A1, TOPREAL1:12;

A9: now

A10: LSeg p1,p2 = (LSeg p1,p) \/ (LSeg p,p2) by A6, TOPREAL1:11;

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

suppose r in LSeg p1,p ; :: thesis: ( (LSeg p1,r) /\ (LSeg r,p) = {r} or (LSeg p,r) /\ (LSeg r,p2) = {r} )

hence ( (LSeg p1,r) /\ (LSeg r,p) = {r} or (LSeg p,r) /\ (LSeg r,p2) = {r} ) by TOPREAL1:14; :: thesis: verum

end;

suppose r in LSeg p,p2 ; :: thesis: ( (LSeg p1,r) /\ (LSeg r,p) = {r} or (LSeg p,r) /\ (LSeg r,p2) = {r} )

hence ( (LSeg p1,r) /\ (LSeg r,p) = {r} or (LSeg p,r) /\ (LSeg r,p2) = {r} ) by TOPREAL1:14; :: thesis: verum

end;

end;

end;

now

assume A11: ( L~ f meets LSeg p1,r & 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 A9;

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

consider x being set such that
A13: ( x in L~ f & x in LSeg p1,r ) by A11, XBOOLE_0:3;
x in (L~ f) /\ (LSeg p1,p2) by A7, A13, XBOOLE_0:def 4;
then x = p by A4, TARSKI:def 1;
then x in LSeg r,p by RLTOPSP1:69;
then x in (LSeg p1,r) /\ (LSeg r,p) by A13, XBOOLE_0:def 4;
hence contradiction by A3, A12, A13, TARSKI:def 1; :: thesis: verum

end;

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

consider x being set such that
A15: ( x in L~ f & x in LSeg r,p2 ) by A11, XBOOLE_0:3;
x in (L~ f) /\ (LSeg p1,p2) by A8, A15, XBOOLE_0:def 4;
then x = p by A4, TARSKI:def 1;
then x in LSeg p,r by RLTOPSP1:69;
then x in (LSeg p,r) /\ (LSeg r,p2) by A15, XBOOLE_0:def 4;
hence contradiction by A3, A14, A15, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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