:: Basic Properties of Connecting Points with Line Segmentsin ${\calE}^2_{\rm T}$
:: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz
::
:: Received August 24, 1992
:: Copyright (c) 1992 Association of Mizar Users
theorem :: TOPREAL3:1
canceled;
theorem :: TOPREAL3:2
canceled;
theorem :: TOPREAL3:3
canceled;
theorem :: TOPREAL3:4
canceled;
theorem :: TOPREAL3:5
canceled;
theorem Th6: :: TOPREAL3:6
theorem Th7: :: TOPREAL3:7
theorem :: TOPREAL3:8
theorem Th9: :: TOPREAL3:9
theorem Th10: :: TOPREAL3:10
theorem Th11: :: TOPREAL3:11
theorem Th12: :: TOPREAL3:12
theorem :: TOPREAL3:13
theorem :: TOPREAL3:14
canceled;
theorem Th15: :: TOPREAL3:15
theorem Th16: :: TOPREAL3:16
theorem :: TOPREAL3:17
theorem :: TOPREAL3:18
theorem :: TOPREAL3:19
theorem :: TOPREAL3:20
theorem Th21: :: TOPREAL3:21
theorem :: TOPREAL3:22
canceled;
theorem :: TOPREAL3:23
theorem Th24: :: TOPREAL3:24
theorem :: TOPREAL3:25
theorem Th26: :: TOPREAL3:26
theorem :: TOPREAL3:27
theorem Th28: :: TOPREAL3:28
theorem :: TOPREAL3:29
for
p1,
p2,
p being
Point of
(TOP-REAL 2) for
r1,
s1,
r2,
s2,
r being
real number for
u being
Point of
(Euclid 2) st
u = p1 &
p1 = |[r1,s1]| &
p2 = |[r2,s2]| &
p = |[r2,s1]| &
p2 in Ball u,
r holds
p in Ball u,
r
theorem :: TOPREAL3:30
theorem :: TOPREAL3:31
theorem :: TOPREAL3:32
for
r1,
r2,
r,
s1,
s2 being
real number for
u being
Point of
(Euclid 2) st
|[r1,r2]| in Ball u,
r &
|[s1,s2]| in Ball u,
r & not
|[r1,s2]| in Ball u,
r holds
|[s1,r2]| in Ball u,
r
theorem :: TOPREAL3:33
theorem :: TOPREAL3:34
theorem :: TOPREAL3:35
theorem Th36: :: TOPREAL3:36
theorem Th37: :: TOPREAL3:37
theorem Th38: :: TOPREAL3:38
theorem Th39: :: TOPREAL3:39
theorem :: TOPREAL3:40
theorem :: TOPREAL3:41
theorem :: TOPREAL3:42
theorem :: TOPREAL3:43
theorem :: TOPREAL3:44
theorem :: TOPREAL3:45
theorem :: TOPREAL3:46
theorem :: TOPREAL3:47
theorem :: TOPREAL3:48
theorem :: TOPREAL3:49
theorem :: TOPREAL3:50
for
p1,
p,
q being
Point of
(TOP-REAL 2) for
r being
real number for
u being
Point of
(Euclid 2) st not
p1 in Ball u,
r &
p in Ball u,
r &
|[(p `1 ),(q `2 )]| in Ball u,
r & not
|[(p `1 ),(q `2 )]| in LSeg p1,
p &
p1 `1 = p `1 &
p `1 <> q `1 &
p `2 <> q `2 holds
((LSeg p,|[(p `1 ),(q `2 )]|) \/ (LSeg |[(p `1 ),(q `2 )]|,q)) /\ (LSeg p1,p) = {p}
theorem :: TOPREAL3:51
for
p1,
p,
q being
Point of
(TOP-REAL 2) for
r being
real number for
u being
Point of
(Euclid 2) st not
p1 in Ball u,
r &
p in Ball u,
r &
|[(q `1 ),(p `2 )]| in Ball u,
r & not
|[(q `1 ),(p `2 )]| in LSeg p1,
p &
p1 `2 = p `2 &
p `1 <> q `1 &
p `2 <> q `2 holds
((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) = {p}