let p, q be Point of (TOP-REAL 2); (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) = {|[(q `1),(p `2)]|}
set p3 = |[(q `1),(p `2)]|;
set l23 = LSeg (p,|[(q `1),(p `2)]|);
set l = LSeg (|[(q `1),(p `2)]|,q);
thus
(LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) c= {|[(q `1),(p `2)]|}
XBOOLE_0:def 10 {|[(q `1),(p `2)]|} c= (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q))proof
let x be
object ;
TARSKI:def 3 ( not x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) or x in {|[(q `1),(p `2)]|} )
assume A1:
x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q))
;
x in {|[(q `1),(p `2)]|}
then
x in LSeg (
p,
|[(q `1),(p `2)]|)
by XBOOLE_0:def 4;
then consider d1 being
Real such that A2:
x = ((1 - d1) * p) + (d1 * |[(q `1),(p `2)]|)
and
0 <= d1
and
d1 <= 1
;
x in LSeg (
|[(q `1),(p `2)]|,
q)
by A1, XBOOLE_0:def 4;
then consider d2 being
Real such that A3:
x = ((1 - d2) * |[(q `1),(p `2)]|) + (d2 * q)
and
0 <= d2
and
d2 <= 1
;
set t =
((1 - d1) * p) + (d1 * |[(q `1),(p `2)]|);
A4:
(((1 - d1) * p) + (d1 * |[(q `1),(p `2)]|)) `2 =
(((1 - d1) * p) `2) + ((d1 * |[(q `1),(p `2)]|) `2)
by Th2
.=
((1 - d1) * (p `2)) + ((d1 * |[(q `1),(p `2)]|) `2)
by Th4
.=
((1 - d1) * (p `2)) + (d1 * (|[(q `1),(p `2)]| `2))
by Th4
.=
((1 - d1) * (|[(q `1),(p `2)]| `2)) + (d1 * (|[(q `1),(p `2)]| `2))
by EUCLID:52
.=
|[(q `1),(p `2)]| `2
;
(((1 - d1) * p) + (d1 * |[(q `1),(p `2)]|)) `1 =
(((1 - d2) * |[(q `1),(p `2)]|) `1) + ((d2 * q) `1)
by A2, A3, Th2
.=
((1 - d2) * (|[(q `1),(p `2)]| `1)) + ((d2 * q) `1)
by Th4
.=
((1 - d2) * (|[(q `1),(p `2)]| `1)) + (d2 * (q `1))
by Th4
.=
((1 - d2) * (|[(q `1),(p `2)]| `1)) + (d2 * (|[(q `1),(p `2)]| `1))
by EUCLID:52
.=
|[(q `1),(p `2)]| `1
;
then
((1 - d1) * p) + (d1 * |[(q `1),(p `2)]|) = |[(q `1),(p `2)]|
by A4, Th6;
hence
x in {|[(q `1),(p `2)]|}
by A2, TARSKI:def 1;
verum
end;
let x be object ; TARSKI:def 3 ( not x in {|[(q `1),(p `2)]|} or x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) )
assume
x in {|[(q `1),(p `2)]|}
; x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q))
then A5:
x = |[(q `1),(p `2)]|
by TARSKI:def 1;
( |[(q `1),(p `2)]| in LSeg (p,|[(q `1),(p `2)]|) & |[(q `1),(p `2)]| in LSeg (|[(q `1),(p `2)]|,q) )
by RLTOPSP1:68;
hence
x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q))
by A5, XBOOLE_0:def 4; verum