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

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄ being Point of (TOP-REAL b₁) st b₂ is_an_arc_of b₃,b₄ holds
ex b₅ being Function of I[01] ,(TOP-REAL b₁) st
( b₅ is continuous & b₅ is one-to-one & rng b₅ = b₂ & b₅ . 0 = b₃ & b₅ . 1 = b₄ )

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃, b₄, b₅ being real number st b₁ `1 < b<sub>3</sub> & b<sub>1</sub> `1 = b₂ `1 & b<sub>4</sub> <= b<sub>1</sub> `2 & b₁ `2 < b<sub>2</sub> `2 & b₂ `2 <= b<sub>5</sub> holds
LE b<sub>1</sub>,b<sub>2</sub>, rectangle (b<sub>1</sub> `1 ),b₃,b₄,b₅

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃, b₄ being real number st b₁ `1 < b<sub>3</sub> & b<sub>4</sub> < b<sub>2</sub> `2 & b₄ <= b₁ `2 & b<sub>1</sub> `2 <= b₂ `2 & b<sub>1</sub> `1 <= b₂ `1 & b<sub>2</sub> `1 <= b₃ holds
LE b₁,b₂, rectangle (b₁ `1 ),b<sub>3</sub>,b<sub>4</sub>,(b<sub>2</sub> `2 )

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

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃, b₄ being real number st b₂ `2 < b<sub>4</sub> & b<sub>2</sub> `2 <= b₁ `2 & b<sub>1</sub> `2 <= b₄ & b₁ `1 < b<sub>2</sub> `1 & b₂ `1 <= b<sub>3</sub> holds
LE b<sub>1</sub>,b<sub>2</sub>, rectangle (b<sub>1</sub> `1 ),b₃,(b₂ `2 ),b₄

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃, b₄, b₅, b₆ being real number st b₃ < b₄ & b₅ < b₆ & b₁ `2 = b<sub>6</sub> & b<sub>2</sub> `2 = b₆ & b₃ <= b₁ `1 & b<sub>1</sub> `1 < b₂ `1 & b<sub>2</sub> `1 <= b₄ holds
LE b₁,b₂, rectangle b₃,b₄,b₅,b₆

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃, b₄, b₅, b₆ being real number st b₃ < b₄ & b₅ < b₆ & b₁ `2 = b<sub>6</sub> & b<sub>2</sub> `1 = b₄ & b₃ <= b₁ `1 & b<sub>1</sub> `1 <= b₄ & b₅ <= b₂ `2 & b<sub>2</sub> `2 <= b₆ holds
LE b₁,b₂, rectangle b₃,b₄,b₅,b₆

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃, b₄, b₅, b₆ being real number st b₃ < b₄ & b₅ < b₆ & b₁ `2 = b<sub>6</sub> & b<sub>2</sub> `2 = b₅ & b₃ <= b₁ `1 & b<sub>1</sub> `1 <= b₄ & b₃ < b₂ `1 & b<sub>2</sub> `1 <= b₄ holds
LE b₁,b₂, rectangle b₃,b₄,b₅,b₆

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃, b₄, b₅, b₆ being real number st b₃ < b₄ & b₅ < b₆ & b₁ `1 = b<sub>4</sub> & b<sub>2</sub> `1 = b₄ & b₅ <= b₂ `2 & b<sub>2</sub> `2 < b₁ `2 & b<sub>1</sub> `2 <= b₆ holds
LE b₁,b₂, rectangle b₃,b₄,b₅,b₆

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃, b₄, b₅, b₆ being real number st b₃ < b₄ & b₅ < b₆ & b₁ `1 = b<sub>4</sub> & b<sub>2</sub> `2 = b₅ & b₅ <= b₁ `2 & b<sub>1</sub> `2 <= b₆ & b₃ < b₂ `1 & b<sub>2</sub> `1 <= b₄ holds
LE b₁,b₂, rectangle b₃,b₄,b₅,b₆

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃, b₄, b₅, b₆ being real number st b₃ < b₄ & b₅ < b₆ & b₁ `2 = b<sub>5</sub> & b<sub>2</sub> `2 = b₅ & b₃ < b₂ `1 & b<sub>2</sub> `1 < b₁ `1 & b<sub>1</sub> `1 <= b₄ holds
LE b₁,b₂, rectangle b₃,b₄,b₅,b₆

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃, b₄, b₅, b₆ being real number st b₃ < b₄ & b₅ < b₆ & b₁ `2 = b<sub>6</sub> & b<sub>2</sub> `1 = b₄ & b₃ <= b₁ `1 & b<sub>1</sub> `1 <= b₄ & b₅ <= b₂ `2 & b<sub>2</sub> `2 <= b₆ holds
LE b₁,b₂, rectangle b₃,b₄,b₅,b₆

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₅ & b₃ `1 = b<sub>5</sub> & b<sub>4</sub> `1 = b₅ & b₇ <= b₁ `2 & b<sub>1</sub> `2 < b₂ `2 & b<sub>2</sub> `2 < b₃ `2 & b<sub>3</sub> `2 < b₄ `2 & b<sub>4</sub> `2 <= b₈ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₅ & b₃ `1 = b<sub>5</sub> & b<sub>4</sub> `2 = b₈ & b₇ <= b₁ `2 & b<sub>1</sub> `2 < b₂ `2 & b<sub>2</sub> `2 < b₃ `2 & b<sub>3</sub> `2 <= b₈ & b₅ <= b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₅ & b₃ `1 = b<sub>5</sub> & b<sub>4</sub> `1 = b₆ & b₇ <= b₁ `2 & b<sub>1</sub> `2 < b₂ `2 & b<sub>2</sub> `2 < b₃ `2 & b<sub>3</sub> `2 <= b₈ & b₇ <= b₄ `2 & b<sub>4</sub> `2 <= b₈ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₅ & b₃ `1 = b<sub>5</sub> & b<sub>4</sub> `2 = b₇ & b₇ <= b₁ `2 & b<sub>1</sub> `2 < b₂ `2 & b<sub>2</sub> `2 < b₃ `2 & b<sub>3</sub> `2 <= b₈ & b₅ < b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₅ & b₃ `2 = b<sub>8</sub> & b<sub>4</sub> `2 = b₈ & b₇ <= b₁ `2 & b<sub>1</sub> `2 < b₂ `2 & b<sub>2</sub> `2 <= b₈ & b₅ <= b₃ `1 & b<sub>3</sub> `1 < b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₅ & b₃ `2 = b<sub>8</sub> & b<sub>4</sub> `1 = b₆ & b₇ <= b₁ `2 & b<sub>1</sub> `2 < b₂ `2 & b<sub>2</sub> `2 <= b₈ & b₅ <= b₃ `1 & b<sub>3</sub> `1 <= b₆ & b₇ <= b₄ `2 & b<sub>4</sub> `2 <= b₈ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₅ & b₃ `2 = b<sub>8</sub> & b<sub>4</sub> `2 = b₇ & b₇ <= b₁ `2 & b<sub>1</sub> `2 < b₂ `2 & b<sub>2</sub> `2 <= b₈ & b₅ <= b₃ `1 & b<sub>3</sub> `1 <= b₆ & b₅ < b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₅ & b₃ `1 = b<sub>6</sub> & b<sub>4</sub> `1 = b₆ & b₇ <= b₁ `2 & b<sub>1</sub> `2 < b₂ `2 & b<sub>2</sub> `2 <= b₈ & b₇ <= b₄ `2 & b<sub>4</sub> `2 < b₃ `2 & b<sub>3</sub> `2 <= b₈ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₅ & b₃ `1 = b<sub>6</sub> & b<sub>4</sub> `2 = b₇ & b₇ <= b₁ `2 & b<sub>1</sub> `2 < b₂ `2 & b<sub>2</sub> `2 <= b₈ & b₇ <= b₃ `2 & b<sub>3</sub> `2 <= b₈ & b₅ < b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₅ & b₃ `2 = b<sub>7</sub> & b<sub>4</sub> `2 = b₇ & b₇ <= b₁ `2 & b<sub>1</sub> `2 < b₂ `2 & b<sub>2</sub> `2 <= b₈ & b₅ < b₄ `1 & b<sub>4</sub> `1 < b₃ `1 & b<sub>3</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `2 = b₈ & b₃ `2 = b<sub>8</sub> & b<sub>4</sub> `2 = b₈ & b₇ <= b₁ `2 & b<sub>1</sub> `2 <= b₈ & b₅ <= b₂ `1 & b<sub>2</sub> `1 < b₃ `1 & b<sub>3</sub> `1 < b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `2 = b₈ & b₃ `2 = b<sub>8</sub> & b<sub>4</sub> `1 = b₆ & b₇ <= b₁ `2 & b<sub>1</sub> `2 <= b₈ & b₅ <= b₂ `1 & b<sub>2</sub> `1 < b₃ `1 & b<sub>3</sub> `1 <= b₆ & b₇ <= b₄ `2 & b<sub>4</sub> `2 <= b₈ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `2 = b₈ & b₃ `2 = b<sub>8</sub> & b<sub>4</sub> `2 = b₇ & b₇ <= b₁ `2 & b<sub>1</sub> `2 <= b₈ & b₅ <= b₂ `1 & b<sub>2</sub> `1 < b₃ `1 & b<sub>3</sub> `1 <= b₆ & b₅ < b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `2 = b₈ & b₃ `1 = b<sub>6</sub> & b<sub>4</sub> `1 = b₆ & b₇ <= b₁ `2 & b<sub>1</sub> `2 <= b₈ & b₅ <= b₂ `1 & b<sub>2</sub> `1 <= b₆ & b₇ <= b₄ `2 & b<sub>4</sub> `2 < b₃ `2 & b<sub>3</sub> `2 <= b₈ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

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

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `2 = b₈ & b₃ `2 = b<sub>7</sub> & b<sub>4</sub> `2 = b₇ & b₇ <= b₁ `2 & b<sub>1</sub> `2 <= b₈ & b₅ <= b₂ `1 & b<sub>2</sub> `1 <= b₆ & b₅ < b₄ `1 & b<sub>4</sub> `1 < b₃ `1 & b<sub>3</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₆ & b₃ `1 = b<sub>6</sub> & b<sub>4</sub> `1 = b₆ & b₇ <= b₁ `2 & b<sub>1</sub> `2 <= b₈ & b₈ >= b₂ `2 & b<sub>2</sub> `2 > b₃ `2 & b<sub>3</sub> `2 > b₄ `2 & b<sub>4</sub> `2 >= b₇ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₆ & b₃ `1 = b<sub>6</sub> & b<sub>4</sub> `2 = b₇ & b₇ <= b₁ `2 & b<sub>1</sub> `2 <= b₈ & b₈ >= b₂ `2 & b<sub>2</sub> `2 > b₃ `2 & b<sub>3</sub> `2 >= b₇ & b₅ < b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `1 = b₆ & b₃ `2 = b<sub>7</sub> & b<sub>4</sub> `2 = b₇ & b₇ <= b₁ `2 & b<sub>1</sub> `2 <= b₈ & b₇ <= b₂ `2 & b<sub>2</sub> `2 <= b₈ & b₅ < b₄ `1 & b<sub>4</sub> `1 < b₃ `1 & b<sub>3</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>5</sub> & b<sub>2</sub> `2 = b₇ & b₃ `2 = b<sub>7</sub> & b<sub>4</sub> `2 = b₇ & b₇ <= b₁ `2 & b<sub>1</sub> `2 <= b₈ & b₅ < b₄ `1 & b<sub>4</sub> `1 < b₃ `1 & b<sub>3</sub> `1 < b₂ `1 & b<sub>2</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `2 = b<sub>8</sub> & b<sub>2</sub> `2 = b₈ & b₃ `2 = b<sub>8</sub> & b<sub>4</sub> `2 = b₈ & b₅ <= b₁ `1 & b<sub>1</sub> `1 < b₂ `1 & b<sub>2</sub> `1 < b₃ `1 & b<sub>3</sub> `1 < b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `2 = b<sub>8</sub> & b<sub>2</sub> `2 = b₈ & b₃ `2 = b<sub>8</sub> & b<sub>4</sub> `1 = b₆ & b₅ <= b₁ `1 & b<sub>1</sub> `1 < b₂ `1 & b<sub>2</sub> `1 < b₃ `1 & b<sub>3</sub> `1 <= b₆ & b₇ <= b₄ `2 & b<sub>4</sub> `2 <= b₈ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `2 = b<sub>8</sub> & b<sub>2</sub> `2 = b₈ & b₃ `2 = b<sub>8</sub> & b<sub>4</sub> `2 = b₇ & b₅ <= b₁ `1 & b<sub>1</sub> `1 < b₂ `1 & b<sub>2</sub> `1 < b₃ `1 & b<sub>3</sub> `1 <= b₆ & b₅ < b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `2 = b<sub>8</sub> & b<sub>2</sub> `2 = b₈ & b₃ `1 = b<sub>6</sub> & b<sub>4</sub> `1 = b₆ & b₅ <= b₁ `1 & b<sub>1</sub> `1 < b₂ `1 & b<sub>2</sub> `1 <= b₆ & b₇ <= b₄ `2 & b<sub>4</sub> `2 < b₃ `2 & b<sub>3</sub> `2 <= b₈ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `2 = b<sub>8</sub> & b<sub>2</sub> `2 = b₈ & b₃ `1 = b<sub>6</sub> & b<sub>4</sub> `2 = b₇ & b₅ <= b₁ `1 & b<sub>1</sub> `1 < b₂ `1 & b<sub>2</sub> `1 <= b₆ & b₇ <= b₃ `2 & b<sub>3</sub> `2 <= b₈ & b₅ < b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `2 = b<sub>8</sub> & b<sub>2</sub> `2 = b₈ & b₃ `2 = b<sub>7</sub> & b<sub>4</sub> `2 = b₇ & b₅ <= b₁ `1 & b<sub>1</sub> `1 < b₂ `1 & b<sub>2</sub> `1 <= b₆ & b₅ < b₄ `1 & b<sub>4</sub> `1 < b₃ `1 & b<sub>3</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `2 = b<sub>8</sub> & b<sub>2</sub> `1 = b₆ & b₃ `1 = b<sub>6</sub> & b<sub>4</sub> `1 = b₆ & b₅ <= b₁ `1 & b<sub>1</sub> `1 <= b₆ & b₈ >= b₂ `2 & b<sub>2</sub> `2 > b₃ `2 & b<sub>3</sub> `2 > b₄ `2 & b<sub>4</sub> `2 >= b₇ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `2 = b<sub>8</sub> & b<sub>2</sub> `1 = b₆ & b₃ `1 = b<sub>6</sub> & b<sub>4</sub> `2 = b₇ & b₅ <= b₁ `1 & b<sub>1</sub> `1 <= b₆ & b₈ >= b₂ `2 & b<sub>2</sub> `2 > b₃ `2 & b<sub>3</sub> `2 >= b₇ & b₅ < b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `2 = b<sub>8</sub> & b<sub>2</sub> `1 = b₆ & b₃ `2 = b<sub>7</sub> & b<sub>4</sub> `2 = b₇ & b₅ <= b₁ `1 & b<sub>1</sub> `1 <= b₆ & b₇ <= b₂ `2 & b<sub>2</sub> `2 <= b₈ & b₅ < b₄ `1 & b<sub>4</sub> `1 < b₃ `1 & b<sub>3</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `2 = b<sub>8</sub> & b<sub>2</sub> `2 = b₇ & b₃ `2 = b<sub>7</sub> & b<sub>4</sub> `2 = b₇ & b₅ <= b₁ `1 & b<sub>1</sub> `1 <= b₆ & b₅ < b₄ `1 & b<sub>4</sub> `1 < b₃ `1 & b<sub>3</sub> `1 < b₂ `1 & b<sub>2</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>6</sub> & b<sub>2</sub> `1 = b₆ & b₃ `1 = b<sub>6</sub> & b<sub>4</sub> `1 = b₆ & b₈ >= b₁ `2 & b<sub>1</sub> `2 > b₂ `2 & b<sub>2</sub> `2 > b₃ `2 & b<sub>3</sub> `2 > b₄ `2 & b<sub>4</sub> `2 >= b₇ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>6</sub> & b<sub>2</sub> `1 = b₆ & b₃ `1 = b<sub>6</sub> & b<sub>4</sub> `2 = b₇ & b₈ >= b₁ `2 & b<sub>1</sub> `2 > b₂ `2 & b<sub>2</sub> `2 > b₃ `2 & b<sub>3</sub> `2 >= b₇ & b₅ < b₄ `1 & b<sub>4</sub> `1 <= b₆ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>6</sub> & b<sub>2</sub> `1 = b₆ & b₃ `2 = b<sub>7</sub> & b<sub>4</sub> `2 = b₇ & b₈ >= b₁ `2 & b<sub>1</sub> `2 > b₂ `2 & b<sub>2</sub> `2 >= b₇ & b₆ >= b₃ `1 & b<sub>3</sub> `1 > b₄ `1 & b<sub>4</sub> `1 > b₅ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `1 = b<sub>6</sub> & b<sub>2</sub> `2 = b₇ & b₃ `2 = b<sub>7</sub> & b<sub>4</sub> `2 = b₇ & b₇ <= b₁ `2 & b<sub>1</sub> `2 <= b₈ & b₆ >= b₂ `1 & b<sub>2</sub> `1 > b₃ `1 & b<sub>3</sub> `1 > b₄ `1 & b<sub>4</sub> `1 > b₅ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆, b₇, b₈ being real number st b₅ < b₆ & b₇ < b₈ & b₁ `2 = b<sub>7</sub> & b<sub>2</sub> `2 = b₇ & b₃ `2 = b<sub>7</sub> & b<sub>4</sub> `2 = b₇ & b₆ >= b₁ `1 & b<sub>1</sub> `1 > b₂ `1 & b<sub>2</sub> `1 > b₃ `1 & b<sub>3</sub> `1 > b₄ `1 & b<sub>4</sub> `1 > b₅ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle b₅,b₆,b₇,b₈

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being Function of (TOP-REAL 2),(TOP-REAL 2) st b₁ > 0 & b₃ > 0 & b₅ = AffineMap b₁,b₂,b₃,b₄ & b₆ = AffineMap (1 / b₁),(- (b₂ / b₁)),(1 / b₃),(- (b₄ / b₃)) holds
( b₆ = b₅ " & b₅ = b₆ " )

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2) st b₁ > 0 & b₃ > 0 & b₅ = AffineMap b₁,b₂,b₃,b₄ holds
( b₅ is_homeomorphism & ( for b₆, b₇ being Point of (TOP-REAL 2) st b₆ `1 < b<sub>7</sub> `1 holds
(b₅ . b₆) `1 < (b<sub>5</sub> . b<sub>7</sub>) `1 ) )

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2) st b₁ > 0 & b₃ > 0 & b₅ = AffineMap b₁,b₂,b₃,b₄ holds
( b₅ is_homeomorphism & ( for b₆, b₇ being Point of (TOP-REAL 2) st b₆ `2 < b<sub>7</sub> `2 holds
(b₅ . b₆) `2 < (b<sub>5</sub> . b<sub>7</sub>) `2 ) )

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2)
for b₆ being Function of I[01] ,(TOP-REAL 2) st b₁ < b₂ & b₃ < b₄ & b₅ = AffineMap (2 / (b₂ - b₁)),(- ((b₂ + b₁) / (b₂ - b₁))),(2 / (b₄ - b₃)),(- ((b₄ + b₃) / (b₄ - b₃))) & rng b₆ c= closed_inside_of_rectangle b₁,b₂,b₃,b₄ holds
rng (b₅ * b₆) c= closed_inside_of_rectangle (- 1),1,(- 1),1

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2)
for b₆ being Function of I[01] ,(TOP-REAL 2) st b₁ < b₂ & b₃ < b₄ & b₅ = AffineMap (2 / (b₂ - b₁)),(- ((b₂ + b₁) / (b₂ - b₁))),(2 / (b₄ - b₃)),(- ((b₄ + b₃) / (b₄ - b₃))) & b₆ is continuous & b₆ is one-to-one holds
( b₅ * b₆ is continuous & b₅ * b₆ is one-to-one )

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2)
for b₆ being Function of I[01] ,(TOP-REAL 2)
for b₇ being Point of I[01] st b₁ < b₂ & b₃ < b₄ & b₅ = AffineMap (2 / (b₂ - b₁)),(- ((b₂ + b₁) / (b₂ - b₁))),(2 / (b₄ - b₃)),(- ((b₄ + b₃) / (b₄ - b₃))) & (b₆ . b₇) `1 = b<sub>1</sub> holds
((b<sub>5</sub> * b<sub>6</sub>) . b<sub>7</sub>) `1 = - 1

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2)
for b₆ being Function of I[01] ,(TOP-REAL 2)
for b₇ being Point of I[01] st b₁ < b₂ & b₃ < b₄ & b₅ = AffineMap (2 / (b₂ - b₁)),(- ((b₂ + b₁) / (b₂ - b₁))),(2 / (b₄ - b₃)),(- ((b₄ + b₃) / (b₄ - b₃))) & (b₆ . b₇) `2 = b<sub>4</sub> holds
((b<sub>5</sub> * b<sub>6</sub>) . b<sub>7</sub>) `2 = 1

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2)
for b₆ being Function of I[01] ,(TOP-REAL 2)
for b₇ being Point of I[01] st b₁ < b₂ & b₃ < b₄ & b₅ = AffineMap (2 / (b₂ - b₁)),(- ((b₂ + b₁) / (b₂ - b₁))),(2 / (b₄ - b₃)),(- ((b₄ + b₃) / (b₄ - b₃))) & (b₆ . b₇) `1 = b<sub>2</sub> holds
((b<sub>5</sub> * b<sub>6</sub>) . b<sub>7</sub>) `1 = 1

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2)
for b₆ being Function of I[01] ,(TOP-REAL 2)
for b₇ being Point of I[01] st b₁ < b₂ & b₃ < b₄ & b₅ = AffineMap (2 / (b₂ - b₁)),(- ((b₂ + b₁) / (b₂ - b₁))),(2 / (b₄ - b₃)),(- ((b₄ + b₃) / (b₄ - b₃))) & (b₆ . b₇) `2 = b<sub>3</sub> holds
((b<sub>5</sub> * b<sub>6</sub>) . b<sub>7</sub>) `2 = - 1

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2)
for b₆ being Function of I[01] ,(TOP-REAL 2)
for b₇, b₈ being Point of I[01] st b₁ < b₂ & b₃ < b₄ & b₅ = AffineMap (2 / (b₂ - b₁)),(- ((b₂ + b₁) / (b₂ - b₁))),(2 / (b₄ - b₃)),(- ((b₄ + b₃) / (b₄ - b₃))) & b₃ <= (b₆ . b₇) `2 & (b<sub>6</sub> . b<sub>7</sub>) `2 < (b₆ . b₈) `2 & (b<sub>6</sub> . b<sub>8</sub>) `2 <= b₄ holds
( - 1 <= ((b₅ * b₆) . b₇) `2 & ((b<sub>5</sub> * b<sub>6</sub>) . b<sub>7</sub>) `2 < ((b₅ * b₆) . b₈) `2 & ((b<sub>5</sub> * b<sub>6</sub>) . b<sub>8</sub>) `2 <= 1 )

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2)
for b₆ being Function of I[01] ,(TOP-REAL 2)
for b₇, b₈ being Point of I[01] st b₁ < b₂ & b₃ < b₄ & b₅ = AffineMap (2 / (b₂ - b₁)),(- ((b₂ + b₁) / (b₂ - b₁))),(2 / (b₄ - b₃)),(- ((b₄ + b₃) / (b₄ - b₃))) & b₃ <= (b₆ . b₇) `2 & (b<sub>6</sub> . b<sub>7</sub>) `2 <= b₄ & b₁ <= (b₆ . b₈) `1 & (b<sub>6</sub> . b<sub>8</sub>) `1 <= b₂ holds
( - 1 <= ((b₅ * b₆) . b₇) `2 & ((b<sub>5</sub> * b<sub>6</sub>) . b<sub>7</sub>) `2 <= 1 & - 1 <= ((b₅ * b₆) . b₈) `1 & ((b<sub>5</sub> * b<sub>6</sub>) . b<sub>8</sub>) `1 <= 1 )

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2)
for b₆ being Function of I[01] ,(TOP-REAL 2)
for b₇, b₈ being Point of I[01] st b₁ < b₂ & b₃ < b₄ & b₅ = AffineMap (2 / (b₂ - b₁)),(- ((b₂ + b₁) / (b₂ - b₁))),(2 / (b₄ - b₃)),(- ((b₄ + b₃) / (b₄ - b₃))) & b₃ <= (b₆ . b₇) `2 & (b<sub>6</sub> . b<sub>7</sub>) `2 <= b₄ & b₃ <= (b₆ . b₈) `2 & (b<sub>6</sub> . b<sub>8</sub>) `2 <= b₄ holds
( - 1 <= ((b₅ * b₆) . b₇) `2 & ((b<sub>5</sub> * b<sub>6</sub>) . b<sub>7</sub>) `2 <= 1 & - 1 <= ((b₅ * b₆) . b₈) `2 & ((b<sub>5</sub> * b<sub>6</sub>) . b<sub>8</sub>) `2 <= 1 )

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2)
for b₆ being Function of I[01] ,(TOP-REAL 2)
for b₇, b₈ being Point of I[01] st b₁ < b₂ & b₃ < b₄ & b₅ = AffineMap (2 / (b₂ - b₁)),(- ((b₂ + b₁) / (b₂ - b₁))),(2 / (b₄ - b₃)),(- ((b₄ + b₃) / (b₄ - b₃))) & b₃ <= (b₆ . b₇) `2 & (b<sub>6</sub> . b<sub>7</sub>) `2 <= b₄ & b₁ < (b₆ . b₈) `1 & (b<sub>6</sub> . b<sub>8</sub>) `1 <= b₂ holds
( - 1 <= ((b₅ * b₆) . b₇) `2 & ((b<sub>5</sub> * b<sub>6</sub>) . b<sub>7</sub>) `2 <= 1 & - 1 < ((b₅ * b₆) . b₈) `1 & ((b<sub>5</sub> * b<sub>6</sub>) . b<sub>8</sub>) `1 <= 1 )

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2)
for b₆ being Function of I[01] ,(TOP-REAL 2)
for b₇, b₈ being Point of I[01] st b₁ < b₂ & b₃ < b₄ & b₅ = AffineMap (2 / (b₂ - b₁)),(- ((b₂ + b₁) / (b₂ - b₁))),(2 / (b₄ - b₃)),(- ((b₄ + b₃) / (b₄ - b₃))) & b₁ <= (b₆ . b₇) `1 & (b<sub>6</sub> . b<sub>7</sub>) `1 < (b₆ . b₈) `1 & (b<sub>6</sub> . b<sub>8</sub>) `1 <= b₂ holds
( - 1 <= ((b₅ * b₆) . b₇) `1 & ((b<sub>5</sub> * b<sub>6</sub>) . b<sub>7</sub>) `1 < ((b₅ * b₆) . b₈) `1 & ((b<sub>5</sub> * b<sub>6</sub>) . b<sub>8</sub>) `1 <= 1 )

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2)
for b₆ being Function of I[01] ,(TOP-REAL 2)
for b₇, b₈ being Point of I[01] st b₁ < b₂ & b₃ < b₄ & b₅ = AffineMap (2 / (b₂ - b₁)),(- ((b₂ + b₁) / (b₂ - b₁))),(2 / (b₄ - b₃)),(- ((b₄ + b₃) / (b₄ - b₃))) & b₁ <= (b₆ . b₇) `1 & (b<sub>6</sub> . b<sub>7</sub>) `1 <= b₂ & b₃ <= (b₆ . b₈) `2 & (b<sub>6</sub> . b<sub>8</sub>) `2 <= b₄ holds
( - 1 <= ((b₅ * b₆) . b₇) `1 & ((b<sub>5</sub> * b<sub>6</sub>) . b<sub>7</sub>) `1 <= 1 & - 1 <= ((b₅ * b₆) . b₈) `2 & ((b<sub>5</sub> * b<sub>6</sub>) . b<sub>8</sub>) `2 <= 1 )