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