let p1, p2 be Point of (TOP-REAL 2); 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; 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); ( 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
; ( 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;
p2 in LSeg (p1,p2)
by RLTOPSP1:68;
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 ( 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)
;
contradictionper 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}
;
contradictionconsider 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;
verum end; suppose A16:
(LSeg (p,r)) /\ (LSeg (r,p2)) = {r}
;
contradictionconsider 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;
verum end; end; end;
hence
( L~ f misses LSeg (p1,r) or L~ f misses LSeg (r,p2) )
; verum