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