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