let p1, p2 be Point of (); :: thesis: for f being non constant standard special_circular_sequence
for r being Point of () 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 () 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 (); :: 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 ;
reconsider p = p as Point of () by A4, A5;
A7: now :: thesis: ( (LSeg (p1,r)) /\ (LSeg (r,p)) = {r} or (LSeg (p,r)) /\ (LSeg (r,p2)) = {r} )
A8: LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) by ;
per cases ( r in LSeg (p1,p) or r in LSeg (p,p2) ) by ;
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:8; :: 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:8; :: thesis: verum
end;
end;
end;
p2 in LSeg (p1,p2) by RLTOPSP1:68;
then A9: LSeg (p2,r) c= LSeg (p1,p2) by ;
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then A10: LSeg (p1,r) c= LSeg (p1,p2) by ;
now :: thesis: ( L~ f meets LSeg (p1,r) implies not L~ f meets LSeg (r,p2) )
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 object such that
A14: x in L~ f and
A15: x in LSeg (p1,r) by ;
x in (L~ f) /\ (LSeg (p1,p2)) by ;
then x = p by ;
then x in LSeg (r,p) by RLTOPSP1:68;
then x in (LSeg (p1,r)) /\ (LSeg (r,p)) by ;
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 object such that
A17: x in L~ f and
A18: x in LSeg (r,p2) by ;
x in (L~ f) /\ (LSeg (p1,p2)) by ;
then x = p by ;
then x in LSeg (p,r) by RLTOPSP1:68;
then x in (LSeg (p,r)) /\ (LSeg (r,p2)) by ;
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