let q, p2, p be Point of (TOP-REAL 2); ( q `2 = p2 `2 & p `2 <> p2 `2 implies ((LSeg (p2,|[(p2 `1),(p `2)]|)) \/ (LSeg (|[(p2 `1),(p `2)]|,p))) /\ (LSeg (q,p2)) = {p2} )
assume that
A1:
q `2 = p2 `2
and
A2:
p `2 <> p2 `2
; ((LSeg (p2,|[(p2 `1),(p `2)]|)) \/ (LSeg (|[(p2 `1),(p `2)]|,p))) /\ (LSeg (q,p2)) = {p2}
set p3 = |[(p2 `1),(p `2)]|;
set l23 = LSeg (p2,|[(p2 `1),(p `2)]|);
set l3 = LSeg (|[(p2 `1),(p `2)]|,p);
set l = LSeg (q,p2);
A3:
(LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)) = {}
proof
set x = the
Element of
(LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2));
assume A4:
(LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)) <> {}
;
contradiction
then
the
Element of
(LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)) in LSeg (
|[(p2 `1),(p `2)]|,
p)
by XBOOLE_0:def 4;
then consider s1 being
Real such that A5:
the
Element of
(LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)) = ((1 - s1) * |[(p2 `1),(p `2)]|) + (s1 * p)
and
0 <= s1
and
s1 <= 1
;
the
Element of
(LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)) in LSeg (
q,
p2)
by A4, XBOOLE_0:def 4;
then consider s2 being
Real such that A6:
the
Element of
(LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)) = ((1 - s2) * q) + (s2 * p2)
and
0 <= s2
and
s2 <= 1
;
A7:
(((1 - s1) * |[(p2 `1),(p `2)]|) + (s1 * p)) `2 =
(((1 - s1) * |[(p2 `1),(p `2)]|) `2) + ((s1 * p) `2)
by Th2
.=
((1 - s1) * (|[(p2 `1),(p `2)]| `2)) + ((s1 * p) `2)
by Th4
.=
((1 - s1) * (|[(p2 `1),(p `2)]| `2)) + (s1 * (p `2))
by Th4
.=
((1 - s1) * (p `2)) + (s1 * (p `2))
by EUCLID:52
.=
p `2
;
(((1 - s2) * q) + (s2 * p2)) `2 =
(((1 - s2) * q) `2) + ((s2 * p2) `2)
by Th2
.=
((1 - s2) * (q `2)) + ((s2 * p2) `2)
by Th4
.=
((1 - s2) * (q `2)) + (s2 * (p2 `2))
by Th4
.=
p2 `2
by A1
;
hence
contradiction
by A2, A5, A7, A6;
verum
end;
A8:
(LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2)) = {p2}
proof
thus
(LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2)) c= {p2}
XBOOLE_0:def 10 {p2} c= (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2))proof
let x be
object ;
TARSKI:def 3 ( not x in (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2)) or x in {p2} )
assume A9:
x in (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2))
;
x in {p2}
then
x in LSeg (
p2,
|[(p2 `1),(p `2)]|)
by XBOOLE_0:def 4;
then consider s1 being
Real such that A10:
((1 - s1) * p2) + (s1 * |[(p2 `1),(p `2)]|) = x
and
0 <= s1
and
s1 <= 1
;
x in LSeg (
q,
p2)
by A9, XBOOLE_0:def 4;
then consider s2 being
Real such that A11:
((1 - s2) * q) + (s2 * p2) = x
and
0 <= s2
and
s2 <= 1
;
A12:
(((1 - s2) * q) + (s2 * p2)) `2 =
(((1 - s2) * q) `2) + ((s2 * p2) `2)
by Th2
.=
((1 - s2) * (q `2)) + ((s2 * p2) `2)
by Th4
.=
((1 - s2) * (q `2)) + (s2 * (p2 `2))
by Th4
.=
p2 `2
by A1
;
set t =
((1 - s1) * p2) + (s1 * |[(p2 `1),(p `2)]|);
A13:
(((1 - s1) * p2) + (s1 * |[(p2 `1),(p `2)]|)) `1 =
(((1 - s1) * p2) `1) + ((s1 * |[(p2 `1),(p `2)]|) `1)
by Th2
.=
((1 - s1) * (p2 `1)) + ((s1 * |[(p2 `1),(p `2)]|) `1)
by Th4
.=
((1 - s1) * (p2 `1)) + (s1 * (|[(p2 `1),(p `2)]| `1))
by Th4
.=
((1 - s1) * (p2 `1)) + (s1 * (p2 `1))
by EUCLID:52
.=
p2 `1
;
((1 - s1) * p2) + (s1 * |[(p2 `1),(p `2)]|) =
|[((((1 - s1) * p2) + (s1 * |[(p2 `1),(p `2)]|)) `1),((((1 - s1) * p2) + (s1 * |[(p2 `1),(p `2)]|)) `2)]|
by EUCLID:53
.=
p2
by A10, A13, A11, A12, EUCLID:53
;
hence
x in {p2}
by A10, TARSKI:def 1;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in {p2} or x in (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2)) )
assume
x in {p2}
;
x in (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2))
then A14:
x = p2
by TARSKI:def 1;
(
p2 in LSeg (
p2,
|[(p2 `1),(p `2)]|) &
p2 in LSeg (
q,
p2) )
by RLTOPSP1:68;
hence
x in (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2))
by A14, XBOOLE_0:def 4;
verum
end;
thus ((LSeg (p2,|[(p2 `1),(p `2)]|)) \/ (LSeg (|[(p2 `1),(p `2)]|,p))) /\ (LSeg (q,p2)) =
((LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2))) \/ ((LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)))
by XBOOLE_1:23
.=
{p2}
by A8, A3
; verum