let p, q be Point of (TOP-REAL 2); ( p `1 <> q `1 & p `2 = q `2 implies (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) = {|[(((p `1) + (q `1)) / 2),(p `2)]|} )
assume that
A1:
p `1 <> q `1
and
A2:
p `2 = q `2
; (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) = {|[(((p `1) + (q `1)) / 2),(p `2)]|}
set p3 = |[(((p `1) + (q `1)) / 2),(p `2)]|;
set l23 = LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|);
set l = LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q);
thus
(LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) c= {|[(((p `1) + (q `1)) / 2),(p `2)]|}
XBOOLE_0:def 10 {|[(((p `1) + (q `1)) / 2),(p `2)]|} c= (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q))proof
let x be
object ;
TARSKI:def 3 ( not x in (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) or x in {|[(((p `1) + (q `1)) / 2),(p `2)]|} )
A3:
LSeg (
p,
|[(((p `1) + (q `1)) / 2),(p `2)]|)
= LSeg (
|[(p `1),(p `2)]|,
|[(((p `1) + (q `1)) / 2),(p `2)]|)
by EUCLID:53;
assume A4:
x in (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q))
;
x in {|[(((p `1) + (q `1)) / 2),(p `2)]|}
then A5:
x in LSeg (
|[(((p `1) + (q `1)) / 2),(p `2)]|,
q)
by XBOOLE_0:def 4;
A6:
LSeg (
|[(((p `1) + (q `1)) / 2),(p `2)]|,
q)
= LSeg (
|[(((p `1) + (q `1)) / 2),(q `2)]|,
|[(q `1),(q `2)]|)
by A2, EUCLID:53;
A7:
x in LSeg (
p,
|[(((p `1) + (q `1)) / 2),(p `2)]|)
by A4, XBOOLE_0:def 4;
now x = |[(((p `1) + (q `1)) / 2),(p `2)]|per cases
( p `1 < q `1 or p `1 > q `1 )
by A1, XXREAL_0:1;
suppose A8:
p `1 < q `1
;
x = |[(((p `1) + (q `1)) / 2),(p `2)]|then
p `1 < ((p `1) + (q `1)) / 2
by XREAL_1:226;
then
x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = p `2 & p `1 <= p1 `1 & p1 `1 <= ((p `1) + (q `1)) / 2 ) }
by A7, A3, Th10;
then consider t1 being
Point of
(TOP-REAL 2) such that A9:
t1 = x
and A10:
t1 `2 = p `2
and
p `1 <= t1 `1
and A11:
t1 `1 <= ((p `1) + (q `1)) / 2
;
A12:
t1 `1 <= |[(((p `1) + (q `1)) / 2),(p `2)]| `1
by A11, EUCLID:52;
((p `1) + (q `1)) / 2
< q `1
by A8, XREAL_1:226;
then
x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q `2 & ((p `1) + (q `1)) / 2 <= p2 `1 & p2 `1 <= q `1 ) }
by A5, A6, Th10;
then
ex
t2 being
Point of
(TOP-REAL 2) st
(
t2 = x &
t2 `2 = q `2 &
((p `1) + (q `1)) / 2
<= t2 `1 &
t2 `1 <= q `1 )
;
then
t1 `1 >= |[(((p `1) + (q `1)) / 2),(p `2)]| `1
by A9, EUCLID:52;
then A13:
t1 `1 = |[(((p `1) + (q `1)) / 2),(p `2)]| `1
by A12, XXREAL_0:1;
t1 `2 = |[(((p `1) + (q `1)) / 2),(p `2)]| `2
by A10, EUCLID:52;
hence
x = |[(((p `1) + (q `1)) / 2),(p `2)]|
by A9, A13, Th6;
verum end; suppose A14:
p `1 > q `1
;
x = |[(((p `1) + (q `1)) / 2),(p `2)]|then
p `1 > ((p `1) + (q `1)) / 2
by XREAL_1:226;
then
x in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `2 = p `2 & ((p `1) + (q `1)) / 2 <= p11 `1 & p11 `1 <= p `1 ) }
by A7, A3, Th10;
then consider t1 being
Point of
(TOP-REAL 2) such that A15:
t1 = x
and A16:
t1 `2 = p `2
and A17:
((p `1) + (q `1)) / 2
<= t1 `1
and
t1 `1 <= p `1
;
A18:
|[(((p `1) + (q `1)) / 2),(p `2)]| `1 <= t1 `1
by A17, EUCLID:52;
q `1 < ((p `1) + (q `1)) / 2
by A14, XREAL_1:226;
then
x in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `2 = q `2 & q `1 <= p22 `1 & p22 `1 <= ((p `1) + (q `1)) / 2 ) }
by A5, A6, Th10;
then
ex
t2 being
Point of
(TOP-REAL 2) st
(
t2 = x &
t2 `2 = q `2 &
q `1 <= t2 `1 &
t2 `1 <= ((p `1) + (q `1)) / 2 )
;
then
t1 `1 <= |[(((p `1) + (q `1)) / 2),(p `2)]| `1
by A15, EUCLID:52;
then A19:
t1 `1 = |[(((p `1) + (q `1)) / 2),(p `2)]| `1
by A18, XXREAL_0:1;
t1 `2 = |[(((p `1) + (q `1)) / 2),(p `2)]| `2
by A16, EUCLID:52;
hence
x = |[(((p `1) + (q `1)) / 2),(p `2)]|
by A15, A19, Th6;
verum end;
hence
x in {|[(((p `1) + (q `1)) / 2),(p `2)]|}
by TARSKI:def 1;
verum
end;
let x be object ; TARSKI:def 3 ( not x in {|[(((p `1) + (q `1)) / 2),(p `2)]|} or x in (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) )
assume
x in {|[(((p `1) + (q `1)) / 2),(p `2)]|}
; x in (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q))
then A20:
x = |[(((p `1) + (q `1)) / 2),(p `2)]|
by TARSKI:def 1;
( |[(((p `1) + (q `1)) / 2),(p `2)]| in LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|) & |[(((p `1) + (q `1)) / 2),(p `2)]| in LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q) )
by RLTOPSP1:68;
hence
x in (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q))
by A20, XBOOLE_0:def 4; verum