for b₁, b₂ being real number st b₁ < b₂ holds
( b₁ < (b₁ + b₂) / 2 & (b₁ + b₂) / 2 < b₂ )

for b₁, b₂, b₃ being set holds
( 1 in dom <*b₁,b₂,b₃*> & 2 in dom <*b₁,b₂,b₃*> & 3 in dom <*b₁,b₂,b₃*> )

for b₁, b₂ being Point of (TOP-REAL 2) holds
( (b₁ + b₂) `1 = (b<sub>1</sub> `1 ) + (b₂ `1 ) & (b<sub>1</sub> + b<sub>2</sub>) `2 = (b₁ `2 ) + (b<sub>2</sub> `2 ) )

for b₁, b₂ being Point of (TOP-REAL 2) holds
( (b₁ - b₂) `1 = (b<sub>1</sub> `1 ) - (b₂ `1 ) & (b<sub>1</sub> - b<sub>2</sub>) `2 = (b₁ `2 ) - (b<sub>2</sub> `2 ) )

for b₁ being Point of (TOP-REAL 2)
for b₂ being real number holds
( (b₂ * b₁) `1 = b<sub>2</sub> * (b<sub>1</sub> `1 ) & (b₂ * b₁) `2 = b<sub>2</sub> * (b<sub>1</sub> `2 ) )

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃, b₄, b₅, b₆ being real number st b₁ = <*b₃,b₄*> & b₂ = <*b₅,b₆*> holds
( b₁ + b₂ = <*(b₃ + b₅),(b₄ + b₆)*> & b₁ - b₂ = <*(b₃ - b₅),(b₄ - b₆)*> )

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ `1 = b<sub>2</sub> `1 & b₁ `2 = b<sub>2</sub> `2 holds
b₁ = b₂

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃, b₄ being Point of (Euclid 2) st b₃ = b₁ & b₄ = b₂ holds
(Pitag_dist 2) . b₃,b₄ = sqrt ((((b₁ `1 ) - (b<sub>2</sub> `1 )) ^2 ) + (((b₁ `2 ) - (b<sub>2</sub> `2 )) ^2 ))

for b₁ being Nat holds the carrier of (TOP-REAL b₁) = the carrier of (Euclid b₁)

for b₁, b₂, b₃ being real number st b₁ <= b₂ holds
{ b₄ where B is Point of (TOP-REAL 2) : ( b₄ `1 = b<sub>3</sub> & b<sub>1</sub> <= b<sub>4</sub> `2 & b₄ `2 <= b₂ ) } = LSeg |[b₃,b₁]|,|[b₃,b₂]|

for b₁, b₂, b₃ being real number st b₁ <= b₂ holds
{ b₄ where B is Point of (TOP-REAL 2) : ( b₄ `2 = b<sub>3</sub> & b<sub>1</sub> <= b<sub>4</sub> `1 & b₄ `1 <= b₂ ) } = LSeg |[b₁,b₃]|,|[b₂,b₃]|

for b₁ being Point of (TOP-REAL 2)
for b₂, b₃, b₄ being real number st b₁ in LSeg |[b₂,b₃]|,|[b₂,b₄]| holds
b₁ `1 = b₂

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

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ `1 <> b<sub>2</sub> `1 & b₁ `2 = b<sub>2</sub> `2 holds
|[(((b₁ `1 ) + (b<sub>2</sub> `1 )) / 2),(b₁ `2 )]| in LSeg b₁,b₂

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ `1 = b<sub>2</sub> `1 & b₁ `2 <> b<sub>2</sub> `2 holds
|[(b₁ `1 ),(((b<sub>1</sub> `2 ) + (b₂ `2 )) / 2)]| in LSeg b₁,b₂

for b₁, b₂, b₃ being Point of (TOP-REAL 2)
for b₄ being FinSequence of (TOP-REAL 2)
for b₅, b₆ being Nat st b₄ = <*b₁,b₂,b₃*> & b₅ <> 0 & b₆ > b₅ + 1 holds
LSeg b₄,b₆ = {}

for b₁, b₂, b₃ being Point of (TOP-REAL 2)
for b₄ being FinSequence of (TOP-REAL 2) st b₄ = <*b₁,b₂,b₃*> holds
L~ b₄ = (LSeg b₁,b₂) \/ (LSeg b₂,b₃)

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom (b₁ | b₂) & b₃ + 1 in dom (b₁ | b₂) holds
LSeg b₁,b₃ = LSeg (b₁ | b₂),b₃

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Nat st b₃ in dom b₁ & b₃ + 1 in dom b₁ holds
LSeg (b₁ ^ b₂),b₃ = LSeg b₁,b₃

for b₁ being Nat
for b₂ being FinSequence of (TOP-REAL b₁)
for b₃ being Nat holds LSeg b₂,b₃ c= L~ b₂

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat holds L~ (b₁ | b₂) c= L~ b₁

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

for b₁, b₂, b₃ being Point of (TOP-REAL 2)
for b₄, b₅, b₆, b₇, b₈ being real number
for b₉ being Point of (Euclid 2) st b₉ = b₁ & b₁ = |[b₄,b₅]| & b₂ = |[b₆,b₇]| & b₃ = |[b₆,b₅]| & b₂ in Ball b₉,b₈ holds
b₃ in Ball b₉,b₈

for b₁, b₂, b₃, b₄ being real number
for b₅ being Point of (Euclid 2) st |[b₁,b₂]| in Ball b₅,b₃ & |[b₁,b₄]| in Ball b₅,b₃ holds
|[b₁,((b₂ + b₄) / 2)]| in Ball b₅,b₃

for b₁, b₂, b₃, b₄ being real number
for b₅ being Point of (Euclid 2) st |[b₁,b₂]| in Ball b₅,b₃ & |[b₄,b₂]| in Ball b₅,b₃ holds
|[((b₁ + b₄) / 2),b₂]| in Ball b₅,b₃

for b₁, b₂, b₃, b₄, b₅ being real number
for b₆ being Point of (Euclid 2) st b₁ <> b₂ & b₃ <> b₄ & |[b₁,b₄]| in Ball b₆,b₅ & |[b₂,b₃]| in Ball b₆,b₅ & not |[b₁,b₃]| in Ball b₆,b₅ holds
|[b₂,b₄]| in Ball b₆,b₅

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being real number
for b₃ being Point of (Euclid 2)
for b₄ being Nat st not b₁ /. 1 in Ball b₃,b₂ & 1 <= b₄ & b₄ <= (len b₁) - 1 & LSeg b₁,b₄ meets Ball b₃,b₂ & ( for b₅ being Nat st 1 <= b₅ & b₅ <= (len b₁) - 1 & (LSeg b₁,b₅) /\ (Ball b₃,b₂) <> {} holds
b₄ <= b₅ ) holds
not b₁ /. b₄ in Ball b₃,b₂

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₁ `2 = b<sub>2</sub> `2 & b₃ `2 <> b<sub>2</sub> `2 holds
((LSeg b₂,|[(b₂ `1 ),(b<sub>3</sub> `2 )]|) \/ (LSeg |[(b₂ `1 ),(b<sub>3</sub> `2 )]|,b₃)) /\ (LSeg b₁,b₂) = {b₂}

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₁ `1 = b<sub>2</sub> `1 & b₃ `1 <> b<sub>2</sub> `1 holds
((LSeg b₂,|[(b₃ `1 ),(b<sub>2</sub> `2 )]|) \/ (LSeg |[(b₃ `1 ),(b<sub>2</sub> `2 )]|,b₃)) /\ (LSeg b₁,b₂) = {b₂}

for b₁, b₂ being Point of (TOP-REAL 2) holds (LSeg b₁,|[(b₁ `1 ),(b<sub>2</sub> `2 )]|) /\ (LSeg |[(b₁ `1 ),(b<sub>2</sub> `2 )]|,b₂) = {|[(b₁ `1 ),(b<sub>2</sub> `2 )]|}

for b₁, b₂ being Point of (TOP-REAL 2) holds (LSeg b₁,|[(b₂ `1 ),(b<sub>1</sub> `2 )]|) /\ (LSeg |[(b₂ `1 ),(b<sub>1</sub> `2 )]|,b₂) = {|[(b₂ `1 ),(b<sub>1</sub> `2 )]|}

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ `1 = b<sub>2</sub> `1 & b₁ `2 <> b<sub>2</sub> `2 holds
(LSeg b₁,|[(b₁ `1 ),(((b<sub>1</sub> `2 ) + (b₂ `2 )) / 2)]|) /\ (LSeg |[(b<sub>1</sub> `1 ),(((b₁ `2 ) + (b<sub>2</sub> `2 )) / 2)]|,b₂) = {|[(b₁ `1 ),(((b<sub>1</sub> `2 ) + (b₂ `2 )) / 2)]|}

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ `1 <> b<sub>2</sub> `1 & b₁ `2 = b<sub>2</sub> `2 holds
(LSeg b₁,|[(((b₁ `1 ) + (b<sub>2</sub> `1 )) / 2),(b₁ `2 )]|) /\ (LSeg |[(((b<sub>1</sub> `1 ) + (b₂ `1 )) / 2),(b<sub>1</sub> `2 )]|,b₂) = {|[(((b₁ `1 ) + (b<sub>2</sub> `1 )) / 2),(b₁ `2 )]|}

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₂ > 2 & b₂ in dom b₁ & b₁ is_S-Seq holds
b₁ | b₂ is_S-Seq

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being FinSequence of (TOP-REAL 2) st b₁ `1 <> b<sub>2</sub> `1 & b₁ `2 <> b<sub>2</sub> `2 & b₃ = <*b₁,|[(b₁ `1 ),(b<sub>2</sub> `2 )]|,b₂*> holds
( b₃ /. 1 = b₁ & b₃ /. (len b₃) = b₂ & b₃ is_S-Seq )

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being FinSequence of (TOP-REAL 2) st b₁ `1 <> b<sub>2</sub> `1 & b₁ `2 <> b<sub>2</sub> `2 & b₃ = <*b₁,|[(b₂ `1 ),(b<sub>1</sub> `2 )]|,b₂*> holds
( b₃ /. 1 = b₁ & b₃ /. (len b₃) = b₂ & b₃ is_S-Seq )

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being FinSequence of (TOP-REAL 2) st b₁ `1 = b<sub>2</sub> `1 & b₁ `2 <> b<sub>2</sub> `2 & b₃ = <*b₁,|[(b₁ `1 ),(((b<sub>1</sub> `2 ) + (b₂ `2 )) / 2)]|,b₂*> holds
( b₃ /. 1 = b₁ & b₃ /. (len b₃) = b₂ & b₃ is_S-Seq )

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being FinSequence of (TOP-REAL 2) st b₁ `1 <> b<sub>2</sub> `1 & b₁ `2 = b<sub>2</sub> `2 & b₃ = <*b₁,|[(((b₁ `1 ) + (b<sub>2</sub> `1 )) / 2),(b₁ `2 )]|,b₂*> holds
( b₃ /. 1 = b₁ & b₃ /. (len b₃) = b₂ & b₃ is_S-Seq )

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₂ in dom b₁ & b₂ + 1 in dom b₁ holds
L~ (b₁ | (b₂ + 1)) = (L~ (b₁ | b₂)) \/ (LSeg (b₁ /. b₂),(b₁ /. (b₂ + 1)))

for b₁ being Point of (TOP-REAL 2)
for b₂ being FinSequence of (TOP-REAL 2) st len b₂ >= 2 & not b₁ in L~ b₂ holds
for b₃ being Nat st 1 <= b₃ & b₃ <= len b₂ holds
b₂ /. b₃ <> b₁

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being FinSequence of (TOP-REAL 2) st b₁ <> b₂ & (LSeg b₁,b₂) /\ (L~ b₃) = {b₁} holds
not b₂ in L~ b₃

for b₁ being Point of (TOP-REAL 2)
for b₂ being FinSequence of (TOP-REAL 2)
for b₃ being real number
for b₄ being Point of (Euclid 2)
for b₅ being Nat st b₂ is_S-Seq & not b₂ /. 1 in Ball b₄,b₃ & b₁ in Ball b₄,b₃ & b₂ /. (len b₂) in LSeg b₂,b₅ & 1 <= b₅ & b₅ + 1 <= len b₂ & LSeg b₂,b₅ meets Ball b₄,b₃ holds
b₅ + 1 = len b₂

for b₁, b₂, b₃ being Point of (TOP-REAL 2)
for b₄ being real number
for b₅ being Point of (Euclid 2) st not b₁ in Ball b₅,b₄ & b₂ in Ball b₅,b₄ & b₃ in Ball b₅,b₄ & not b₃ in LSeg b₁,b₂ & ( ( b₂ `1 = b<sub>3</sub> `1 & b₂ `2 <> b<sub>3</sub> `2 ) or ( b₂ `1 <> b<sub>3</sub> `1 & b₂ `2 = b<sub>3</sub> `2 ) ) & ( b₁ `1 = b<sub>2</sub> `1 or b₁ `2 = b<sub>2</sub> `2 ) holds
(LSeg b₁,b₂) /\ (LSeg b₂,b₃) = {b₂}

for b₁, b₂, b₃ being Point of (TOP-REAL 2)
for b₄ being real number
for b₅ being Point of (Euclid 2) st not b₁ in Ball b₅,b₄ & b₂ in Ball b₅,b₄ & |[(b₂ `1 ),(b<sub>3</sub> `2 )]| in Ball b₅,b₄ & b₃ in Ball b₅,b₄ & not |[(b₂ `1 ),(b<sub>3</sub> `2 )]| in LSeg b₁,b₂ & b₁ `1 = b<sub>2</sub> `1 & b₂ `1 <> b<sub>3</sub> `1 & b₂ `2 <> b<sub>3</sub> `2 holds
((LSeg b₂,|[(b₂ `1 ),(b<sub>3</sub> `2 )]|) \/ (LSeg |[(b₂ `1 ),(b<sub>3</sub> `2 )]|,b₃)) /\ (LSeg b₁,b₂) = {b₂}

for b₁, b₂, b₃ being Point of (TOP-REAL 2)
for b₄ being real number
for b₅ being Point of (Euclid 2) st not b₁ in Ball b₅,b₄ & b₂ in Ball b₅,b₄ & |[(b₃ `1 ),(b<sub>2</sub> `2 )]| in Ball b₅,b₄ & b₃ in Ball b₅,b₄ & not |[(b₃ `1 ),(b<sub>2</sub> `2 )]| in LSeg b₁,b₂ & b₁ `2 = b<sub>2</sub> `2 & b₂ `1 <> b<sub>3</sub> `1 & b₂ `2 <> b<sub>3</sub> `2 holds
((LSeg b₂,|[(b₃ `1 ),(b<sub>2</sub> `2 )]|) \/ (LSeg |[(b₃ `1 ),(b<sub>2</sub> `2 )]|,b₃)) /\ (LSeg b₁,b₂) = {b₂}