:: TOPREAL9 semantic presentation

theorem Th1: :: TOPREAL9:1

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) holds (b₂ - b₃) - b₄ = (b₂ - b₄) - b₃

proof end;

theorem Th2: :: TOPREAL9:2

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) st b₂ + b₃ = b₂ + b₄ holds
b₃ = b₄

proof end;

theorem Th3: :: TOPREAL9:3

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) st not b₁ is empty holds
b₂ <> b₂ + (1.REAL b₁)

proof end;

theorem Th4: :: TOPREAL9:4

for b₁ being Nat
for b₂ being real number
for b₃, b₄ being Point of (TOP-REAL b₁)
for b₅ being set st b₅ = ((1 - b₂) * b₃) + (b₂ * b₄) holds
( ( not b₅ = b₃ or b₂ = 0 or b₃ = b₄ ) & ( ( b₂ = 0 or b₃ = b₄ ) implies b₅ = b₃ ) & ( not b₅ = b₄ or b₂ = 1 or b₃ = b₄ ) & ( ( b₂ = 1 or b₃ = b₄ ) implies b₅ = b₄ ) )

proof end;

theorem Th5: :: TOPREAL9:5

for b₁ being FinSequence of REAL holds |.b₁.| ^2 = Sum (sqr b₁)

proof end;

theorem Th6: :: TOPREAL9:6

for b₁ being real number
for b₂ being non empty MetrSpace
for b₃, b₄, b₅ being Point of b₂ st b₃ <> b₄ & b₃ in cl_Ball b₅,b₁ & b₄ in cl_Ball b₅,b₁ holds
b₁ > 0

proof end;

definition

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
let c₃ be real number ;
func Ball c₂,c₃ -> Subset of (TOP-REAL a₁) equals :: TOPREAL9:def 1
{ b₁ where B is Point of (TOP-REAL a₁) : |.(b₁ - a₂).| < a₃ } ;
coherence

proof end;

func cl_Ball c₂,c₃ -> Subset of (TOP-REAL a₁) equals :: TOPREAL9:def 2
{ b₁ where B is Point of (TOP-REAL a₁) : |.(b₁ - a₂).| <= a₃ } ;
coherence

proof end;

func Sphere c₂,c₃ -> Subset of (TOP-REAL a₁) equals :: TOPREAL9:def 3
{ b₁ where B is Point of (TOP-REAL a₁) : |.(b₁ - a₂).| = a₃ } ;
coherence

proof end;

end;

:: deftheorem Def1 defines Ball TOPREAL9:def 1 :

:: deftheorem Def2 defines cl_Ball TOPREAL9:def 2 :

:: deftheorem Def3 defines Sphere TOPREAL9:def 3 :

theorem Th7: :: TOPREAL9:7

for b₁ being Nat
for b₂ being real number
for b₃, b₄ being Point of (TOP-REAL b₁) holds
( b₃ in Ball b₄,b₂ iff |.(b₃ - b₄).| < b₂ )

proof end;

theorem Th8: :: TOPREAL9:8

for b₁ being Nat
for b₂ being real number
for b₃, b₄ being Point of (TOP-REAL b₁) holds
( b₃ in cl_Ball b₄,b₂ iff |.(b₃ - b₄).| <= b₂ )

proof end;

theorem Th9: :: TOPREAL9:9

for b₁ being Nat
for b₂ being real number
for b₃, b₄ being Point of (TOP-REAL b₁) holds
( b₃ in Sphere b₄,b₂ iff |.(b₃ - b₄).| = b₂ )

proof end;

theorem Th10: :: TOPREAL9:10

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) st b₃ in Ball (0.REAL b₁),b₂ holds
|.b₃.| < b₂

proof end;

theorem Th11: :: TOPREAL9:11

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) st b₃ in cl_Ball (0.REAL b₁),b₂ holds
|.b₃.| <= b₂

proof end;

theorem Th12: :: TOPREAL9:12

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) st b₃ in Sphere (0.REAL b₁),b₂ holds
|.b₃.| = b₂

proof end;

theorem Th13: :: TOPREAL9:13

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁)
for b₄ being Point of (Euclid b₁) st b₃ = b₄ holds
Ball b₄,b₂ = Ball b₃,b₂

proof end;

theorem Th14: :: TOPREAL9:14

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁)
for b₄ being Point of (Euclid b₁) st b₃ = b₄ holds
cl_Ball b₄,b₂ = cl_Ball b₃,b₂

proof end;

theorem Th15: :: TOPREAL9:15

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁)
for b₄ being Point of (Euclid b₁) st b₃ = b₄ holds
Sphere b₄,b₂ = Sphere b₃,b₂

proof end;

theorem Th16: :: TOPREAL9:16

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) holds Ball b₃,b₂ c= cl_Ball b₃,b₂

proof end;

theorem Th17: :: TOPREAL9:17

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) holds Sphere b₃,b₂ c= cl_Ball b₃,b₂

proof end;

theorem Th18: :: TOPREAL9:18

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) holds (Ball b₃,b₂) \/ (Sphere b₃,b₂) = cl_Ball b₃,b₂

proof end;

theorem Th19: :: TOPREAL9:19

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) holds Ball b₃,b₂ misses Sphere b₃,b₂

proof end;

registration

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
let c₃ be real non positive number ;
cluster Ball a₂,a₃ -> empty ;
coherence

proof end;

end;

registration

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
let c₃ be real positive number ;
cluster Ball a₂,a₃ -> non empty ;
coherence

proof end;

end;

theorem Th20: :: TOPREAL9:20

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) st not Ball b₃,b₂ is empty holds
b₂ > 0

proof end;

theorem Th21: :: TOPREAL9:21

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) st Ball b₃,b₂ is empty holds
b₂ <= 0

proof end;

registration

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
let c₃ be real negative number ;
cluster cl_Ball a₂,a₃ -> empty ;
coherence

proof end;

end;

registration

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
let c₃ be real non negative number ;
cluster cl_Ball a₂,a₃ -> non empty ;
coherence

proof end;

end;

theorem Th22: :: TOPREAL9:22

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) st not cl_Ball b₃,b₂ is empty holds
b₂ >= 0

proof end;

theorem Th23: :: TOPREAL9:23

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) st cl_Ball b₃,b₂ is empty holds
b₂ < 0

proof end;

theorem Th24: :: TOPREAL9:24

for b₁ being Nat
for b₂, b₃, b₄ being real number
for b₅, b₆, b₇ being Point of (TOP-REAL b₁) st b₂ + b₃ = 1 & (abs b₂) + (abs b₃) = 1 & b₃ <> 0 & b₅ in cl_Ball b₆,b₄ & b₇ in Ball b₆,b₄ holds
(b₂ * b₅) + (b₃ * b₇) in Ball b₆,b₄

proof end;

registration

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
let c₃ be real number ;
cluster Ball a₂,a₃ -> open Bounded ;
coherence

proof end;

cluster cl_Ball a₂,a₃ -> closed Bounded ;
coherence

proof end;

cluster Sphere a₂,a₃ -> closed Bounded ;
coherence

proof end;

end;

Lemma18: for b₁ being Nat
for b₂ being real number
for b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) st b₃ = { b₅ where B is Point of (TOP-REAL b₁) : |.(b₅ - b₄).| <= b₂ } holds
b₃ is convex

proof end;

Lemma19: for b₁ being Nat
for b₂ being real number
for b₃ being Subset of (TOP-REAL b₁)
for b₄ being Point of (TOP-REAL b₁) st b₃ = { b₅ where B is Point of (TOP-REAL b₁) : |.(b₅ - b₄).| < b₂ } holds
b₃ is convex

proof end;

registration

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
let c₃ be real number ;
cluster Ball a₂,a₃ -> open Bounded convex ;
coherence by Lemma19;
cluster cl_Ball a₂,a₃ -> closed Bounded convex ;
coherence by Lemma18;

end;

definition

let c₁ be Nat;
let c₂ be Function of (TOP-REAL c₁),(TOP-REAL c₁);
attr a₂ is homogeneous means :Def4: :: TOPREAL9:def 4
for b₁ being real number
for b₂ being Point of (TOP-REAL a₁) holds a₂ . (b₁ * b₂) = b₁ * (a₂ . b₂);
attr a₂ is additive means :Def5: :: TOPREAL9:def 5
for b₁, b₂ being Point of (TOP-REAL a₁) holds a₂ . (b₁ + b₂) = (a₂ . b₁) + (a₂ . b₂);

end;

:: deftheorem Def4 defines homogeneous TOPREAL9:def 4 :

:: deftheorem Def5 defines additive TOPREAL9:def 5 :

registration

let c₁ be Nat;
cluster (TOP-REAL a₁) --> (0.REAL a₁) -> homogeneous additive ;
coherence

proof end;

end;

registration

let c₁ be Nat;
cluster continuous homogeneous additive M5(the carrier of (TOP-REAL a₁),the carrier of (TOP-REAL a₁));
existence

proof end;

end;

registration

let c₁, c₂ be real number ;
cluster AffineMap a₁,0,a₂,0 -> homogeneous additive ;
coherence

proof end;

end;

theorem Th25: :: TOPREAL9:25

for b₁ being Nat
for b₂ being homogeneous additive Function of (TOP-REAL b₁),(TOP-REAL b₁)
for b₃ being convex Subset of (TOP-REAL b₁) holds b₂ .: b₃ is convex

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
func halfline c₂,c₃ -> Subset of (TOP-REAL a₁) equals :: TOPREAL9:def 6
{ (((1 - b₁) * a₂) + (b₁ * a₃)) where B is Real : 0 <= b₁ } ;
coherence

proof end;

end;

:: deftheorem Def6 defines halfline TOPREAL9:def 6 :

theorem Th26: :: TOPREAL9:26

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being set holds
( b₄ in halfline b₂,b₃ iff ex b₅ being real number st
( b₄ = ((1 - b₅) * b₂) + (b₅ * b₃) & 0 <= b₅ ) )

proof end;

registration

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
cluster halfline a₂,a₃ -> non empty ;
coherence

proof end;

end;

theorem Th27: :: TOPREAL9:27

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds b₂ in halfline b₂,b₃

proof end;

theorem Th28: :: TOPREAL9:28

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds b₂ in halfline b₃,b₂

proof end;

theorem Th29: :: TOPREAL9:29

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds halfline b₂,b₂ = {b₂}

proof end;

theorem Th30: :: TOPREAL9:30

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) st b₂ in halfline b₃,b₄ holds
halfline b₃,b₂ c= halfline b₃,b₄

proof end;

theorem Th31: :: TOPREAL9:31

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) st b₂ in halfline b₃,b₄ & b₂ <> b₃ holds
halfline b₃,b₄ = halfline b₃,b₂

proof end;

theorem Th32: :: TOPREAL9:32

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds LSeg b₂,b₃ c= halfline b₂,b₃

proof end;

registration

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
cluster halfline a₂,a₃ -> non empty convex ;
coherence

proof end;

end;

theorem Th33: :: TOPREAL9:33

for b₁ being Nat
for b₂ being real number
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₃ in Sphere b₄,b₂ & b₅ in Ball b₄,b₂ holds
(LSeg b₃,b₅) /\ (Sphere b₄,b₂) = {b₃}

proof end;

theorem Th34: :: TOPREAL9:34

for b₁ being Nat
for b₂ being real number
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₃ in Sphere b₄,b₂ & b₅ in Sphere b₄,b₂ holds
(LSeg b₃,b₅) \ {b₃,b₅} c= Ball b₄,b₂

proof end;

theorem Th35: :: TOPREAL9:35

for b₁ being Nat
for b₂ being real number
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₃ in Sphere b₄,b₂ & b₅ in Sphere b₄,b₂ holds
(LSeg b₃,b₅) /\ (Sphere b₄,b₂) = {b₃,b₅}

proof end;

theorem Th36: :: TOPREAL9:36

for b₁ being Nat
for b₂ being real number
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₃ in Sphere b₄,b₂ & b₅ in Sphere b₄,b₂ holds
(halfline b₃,b₅) /\ (Sphere b₄,b₂) = {b₃,b₅}

proof end;

theorem Th37: :: TOPREAL9:37

for b₁ being Nat
for b₂, b₃ being real number
for b₄, b₅, b₆ being Point of (TOP-REAL b₁)
for b₇, b₈, b₉ being Element of REAL b₁ st b₇ = b₄ & b₈ = b₅ & b₉ = b₆ & b₄ <> b₅ & b₄ in Ball b₆,b₂ & b₃ = ((- (2 * |((b₅ - b₄),(b₄ - b₆))|)) + (sqrt (delta (Sum (sqr (b₈ - b₇))),(2 * |((b₅ - b₄),(b₄ - b₆))|),((Sum (sqr (b₇ - b₉))) - (b₂ ^2 ))))) / (2 * (Sum (sqr (b₈ - b₇)))) holds
ex b₁₀ being Point of (TOP-REAL b₁) st
( {b₁₀} = (halfline b₄,b₅) /\ (Sphere b₆,b₂) & b₁₀ = ((1 - b₃) * b₄) + (b₃ * b₅) )

proof end;

theorem Th38: :: TOPREAL9:38

for b₁ being Nat
for b₂, b₃ being real number
for b₄, b₅, b₆ being Point of (TOP-REAL b₁)
for b₇, b₈, b₉ being Element of REAL b₁ st b₇ = ((1 / 2) * b₄) + ((1 / 2) * b₅) & b₈ = b₅ & b₉ = b₆ & b₄ <> b₅ & b₄ in Sphere b₆,b₂ & b₅ in cl_Ball b₆,b₂ holds
ex b₁₀ being Point of (TOP-REAL b₁) st
( b₁₀ <> b₄ & {b₄,b₁₀} = (halfline b₄,b₅) /\ (Sphere b₆,b₂) & ( b₅ in Sphere b₆,b₂ implies b₁₀ = b₅ ) & ( not b₅ in Sphere b₆,b₂ & b₃ = ((- (2 * |((b₅ - (((1 / 2) * b₄) + ((1 / 2) * b₅))),((((1 / 2) * b₄) + ((1 / 2) * b₅)) - b₆))|)) + (sqrt (delta (Sum (sqr (b₈ - b₇))),(2 * |((b₅ - (((1 / 2) * b₄) + ((1 / 2) * b₅))),((((1 / 2) * b₄) + ((1 / 2) * b₅)) - b₆))|),((Sum (sqr (b₇ - b₉))) - (b₂ ^2 ))))) / (2 * (Sum (sqr (b₈ - b₇)))) implies b₁₀ = ((1 - b₃) * (((1 / 2) * b₄) + ((1 / 2) * b₅))) + (b₃ * b₅) ) )

proof end;

registration

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
let c₃ be real negative number ;
cluster Sphere a₂,a₃ -> empty closed Bounded ;
coherence

proof end;

end;

registration

let c₁ be non empty Nat;
let c₂ be Point of (TOP-REAL c₁);
let c₃ be real non negative number ;
cluster Sphere a₂,a₃ -> non empty closed Bounded ;
coherence

proof end;

end;

theorem Th39: :: TOPREAL9:39

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) st not Sphere b₃,b₂ is empty holds
b₂ >= 0

proof end;

theorem Th40: :: TOPREAL9:40

for b₁ being Nat
for b₂ being real number
for b₃ being Point of (TOP-REAL b₁) st not b₁ is empty & Sphere b₃,b₂ is empty holds
b₂ < 0

proof end;

theorem Th41: :: TOPREAL9:41

for b₁, b₂ being real number
for b₃, b₄ being Point of (TOP-REAL 2) holds ((b₁ * b₃) + (b₂ * b₄)) `1 = (b₁ * (b₃ `1 )) + (b₂ * (b₄ `1 ))

proof end;

theorem Th42: :: TOPREAL9:42

for b₁, b₂ being real number
for b₃, b₄ being Point of (TOP-REAL 2) holds ((b₁ * b₃) + (b₂ * b₄)) `2 = (b₁ * (b₃ `2 )) + (b₂ * (b₄ `2 ))

proof end;

theorem Th43: :: TOPREAL9:43

for b₁, b₂, b₃ being real number
for b₄ being Point of (TOP-REAL 2) holds
( b₄ in circle b₁,b₂,b₃ iff |.(b₄ - |[b₁,b₂]|).| = b₃ )

proof end;

theorem Th44: :: TOPREAL9:44

for b₁, b₂, b₃ being real number
for b₄ being Point of (TOP-REAL 2) holds
( b₄ in closed_inside_of_circle b₁,b₂,b₃ iff |.(b₄ - |[b₁,b₂]|).| <= b₃ )

proof end;

theorem Th45: :: TOPREAL9:45

for b₁, b₂, b₃ being real number
for b₄ being Point of (TOP-REAL 2) holds
( b₄ in inside_of_circle b₁,b₂,b₃ iff |.(b₄ - |[b₁,b₂]|).| < b₃ )

proof end;

registration

let c₁, c₂ be real number ;
let c₃ be real positive number ;
cluster inside_of_circle a₁,a₂,a₃ -> non empty ;
coherence

proof end;

end;

registration

let c₁, c₂ be real number ;
let c₃ be real non negative number ;
cluster closed_inside_of_circle a₁,a₂,a₃ -> non empty ;
coherence

proof end;

end;

theorem Th46: :: TOPREAL9:46

for b₁, b₂, b₃ being real number holds circle b₁,b₂,b₃ c= closed_inside_of_circle b₁,b₂,b₃

proof end;

theorem Th47: :: TOPREAL9:47

for b₁, b₂, b₃ being real number
for b₄ being Point of (Euclid 2) st b₄ = |[b₁,b₂]| holds
cl_Ball b₄,b₃ = closed_inside_of_circle b₁,b₂,b₃

proof end;

theorem Th48: :: TOPREAL9:48

for b₁, b₂, b₃ being real number
for b₄ being Point of (Euclid 2) st b₄ = |[b₁,b₂]| holds
Ball b₄,b₃ = inside_of_circle b₁,b₂,b₃

proof end;

theorem Th49: :: TOPREAL9:49

for b₁, b₂, b₃ being real number
for b₄ being Point of (Euclid 2) st b₄ = |[b₁,b₂]| holds
Sphere b₄,b₃ = circle b₁,b₂,b₃

proof end;

theorem Th50: :: TOPREAL9:50

for b₁, b₂, b₃ being real number holds Ball |[b₁,b₂]|,b₃ = inside_of_circle b₁,b₂,b₃

proof end;

theorem Th51: :: TOPREAL9:51

for b₁, b₂, b₃ being real number holds cl_Ball |[b₁,b₂]|,b₃ = closed_inside_of_circle b₁,b₂,b₃

proof end;

theorem Th52: :: TOPREAL9:52

for b₁, b₂, b₃ being real number holds Sphere |[b₁,b₂]|,b₃ = circle b₁,b₂,b₃

proof end;

theorem Th53: :: TOPREAL9:53

for b₁, b₂, b₃ being real number holds inside_of_circle b₁,b₂,b₃ c= closed_inside_of_circle b₁,b₂,b₃

proof end;

theorem Th54: :: TOPREAL9:54

for b₁, b₂, b₃ being real number holds inside_of_circle b₁,b₂,b₃ misses circle b₁,b₂,b₃

proof end;

theorem Th55: :: TOPREAL9:55

for b₁, b₂, b₃ being real number holds (inside_of_circle b₁,b₂,b₃) \/ (circle b₁,b₂,b₃) = closed_inside_of_circle b₁,b₂,b₃

proof end;

theorem Th56: :: TOPREAL9:56

for b₁ being real number
for b₂ being Point of (TOP-REAL 2) st b₂ in Sphere (0.REAL 2),b₁ holds
((b₂ `1 ) ^2 ) + ((b₂ `2 ) ^2 ) = b₁ ^2

proof end;

theorem Th57: :: TOPREAL9:57

for b₁, b₂, b₃ being real number
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ <> b₅ & b₄ in closed_inside_of_circle b₁,b₂,b₃ & b₅ in closed_inside_of_circle b₁,b₂,b₃ holds
b₃ > 0

proof end;

theorem Th58: :: TOPREAL9:58

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being Point of (TOP-REAL 2)
for b₇, b₈, b₉ being Element of REAL 2 st b₇ = b₅ & b₈ = b₆ & b₉ = |[b₁,b₂]| & b₃ = ((- (2 * |((b₆ - b₅),(b₅ - |[b₁,b₂]|))|)) + (sqrt (delta (Sum (sqr (b₈ - b₇))),(2 * |((b₆ - b₅),(b₅ - |[b₁,b₂]|))|),((Sum (sqr (b₇ - b₉))) - (b₄ ^2 ))))) / (2 * (Sum (sqr (b₈ - b₇)))) & b₅ <> b₆ & b₅ in inside_of_circle b₁,b₂,b₄ holds
ex b₁₀ being Point of (TOP-REAL 2) st
( {b₁₀} = (halfline b₅,b₆) /\ (circle b₁,b₂,b₄) & b₁₀ = ((1 - b₃) * b₅) + (b₃ * b₆) )

proof end;

theorem Th59: :: TOPREAL9:59

for b₁, b₂, b₃ being real number
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ in circle b₁,b₂,b₃ & b₅ in inside_of_circle b₁,b₂,b₃ holds
(LSeg b₄,b₅) /\ (circle b₁,b₂,b₃) = {b₄}

proof end;

theorem Th60: :: TOPREAL9:60

for b₁, b₂, b₃ being real number
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ in circle b₁,b₂,b₃ & b₅ in circle b₁,b₂,b₃ holds
(LSeg b₄,b₅) \ {b₄,b₅} c= inside_of_circle b₁,b₂,b₃

proof end;

theorem Th61: :: TOPREAL9:61

for b₁, b₂, b₃ being real number
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ in circle b₁,b₂,b₃ & b₅ in circle b₁,b₂,b₃ holds
(LSeg b₄,b₅) /\ (circle b₁,b₂,b₃) = {b₄,b₅}

proof end;

theorem Th62: :: TOPREAL9:62

for b₁, b₂, b₃ being real number
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ in circle b₁,b₂,b₃ & b₅ in circle b₁,b₂,b₃ holds
(halfline b₄,b₅) /\ (circle b₁,b₂,b₃) = {b₄,b₅}

proof end;

theorem Th63: :: TOPREAL9:63

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being Point of (TOP-REAL 2)
for b₇, b₈, b₉ being Element of REAL 2 st b₇ = ((1 / 2) * b₅) + ((1 / 2) * b₆) & b₈ = b₆ & b₉ = |[b₁,b₂]| & b₅ <> b₆ & b₅ in circle b₁,b₂,b₃ & b₆ in closed_inside_of_circle b₁,b₂,b₃ holds
ex b₁₀ being Point of (TOP-REAL 2) st
( b₁₀ <> b₅ & {b₅,b₁₀} = (halfline b₅,b₆) /\ (circle b₁,b₂,b₃) & ( b₆ in Sphere |[b₁,b₂]|,b₃ implies b₁₀ = b₆ ) & ( not b₆ in Sphere |[b₁,b₂]|,b₃ & b₄ = ((- (2 * |((b₆ - (((1 / 2) * b₅) + ((1 / 2) * b₆))),((((1 / 2) * b₅) + ((1 / 2) * b₆)) - |[b₁,b₂]|))|)) + (sqrt (delta (Sum (sqr (b₈ - b₇))),(2 * |((b₆ - (((1 / 2) * b₅) + ((1 / 2) * b₆))),((((1 / 2) * b₅) + ((1 / 2) * b₆)) - |[b₁,b₂]|))|),((Sum (sqr (b₇ - b₉))) - (b₃ ^2 ))))) / (2 * (Sum (sqr (b₈ - b₇)))) implies b₁₀ = ((1 - b₄) * (((1 / 2) * b₅) + ((1 / 2) * b₆))) + (b₄ * b₆) ) )

proof end;

registration

let c₁, c₂, c₃ be real number ;
cluster inside_of_circle a₁,a₂,a₃ -> convex ;
coherence

proof end;

cluster closed_inside_of_circle a₁,a₂,a₃ -> convex ;
coherence

proof end;

end;