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;

A7: now

A8: 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, A8, 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;

p2 in LSeg p1,p2 by RLTOPSP1:69;
then A9: LSeg p2,r c= LSeg p1,p2 by A1, TOPREAL1:12;
p1 in LSeg p1,p2 by RLTOPSP1:69;
then A10: LSeg p1,r c= LSeg p1,p2 by A1, TOPREAL1:12;

now

assume that
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;

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

consider x being set 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:69;
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;

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

consider x being set 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:69;
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;

end;

end;

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