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