(* 0

Function definition list:
An(x1) = An(x1)
Zero = Zero
One = One
x1 + x2 = x1 + x2
x1 * x2 = x1 * x2
Minus(x1) = Minus(x1)
Inv(x1) = Inv(x1)
Sup(x1) = Sup(x1)
Nat = {x1|(Ax2.
     Zero E x2 & (Ax3.
     x3 E x2 -> x3 + One E x2) -> x1 E x2)}
Reals = {x1|Real(x1)}
x1
      Closure x2 = {x3|(Ax4.
     x1 E x4 & (Ax5.
     p1(x5) E x4 & x5 E x2 -> p2(x5) E x4)
      -> x3 E x4)}
x1 Union x2 = {x3|x3 E x1 v x3 E x2}
Sing(x1) = {x2|x2 = x1}
x1
      Couple x2 = {x3|x3 = x1 v x3 = x2}
x1 Kpair x2 = 
     Sing(x1) Couple x1 Couple x2
Si(x1) = {x2|(Ax3.
     x3 E x1 -> x2 E x3)}
Projtwo(x1) = {x2|
     (Ex3.x2 E x3 & x3 E x1) & (Ax3.(Ax4.
     x2 E x3 & x2 E x4 & x3 E x1
      & x4 E x1 -> x3 = x4))}
Three = 
     One + One + One
Two = One + One
Half = Inv(Two)*)


(* Sequent snapshot:


1:  (Ax2.
     Zero < x2
      & Real(x2)
      & x2 < Sup({x3|Zero < x3 & x3 * x3 < a1})
      -> [a1
      + Minus(Sup({x70|
     Zero < x70 & x70 * x70 < a1})
      * Sup({x71|
     Zero < x71 & x71 * x71 < a1}))]
      * Inv(
     Three
      * Sup({x72|Zero < x72 & x72 * x72 < a1})) <= x2)

2:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

3:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

4:  Real(a1)

5:  Zero < a1

|-

1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

2:  (Ex3.x3 * x3 = a1)


*)



(* 0

Predicate definition list:
Real(x1) == Real(x1)
x1 < x2 == x1 < x2

     x1 Equal x2
      == x1 + Zero = x2 + Zero
x1 <= x2 == x1 Equal x2
      v x1 < x2
x1 Function x2 == (Ax3.
     x3 E x1
      -> p1(x3) E p1(x2) & p2(x3) E p2(x2)) & (Ax3.(Ax4.(Ax5.
     [x3,x5] E x1
      & [x4,x5] E x1
      -> x3 = x4)))

     Sequence(x1)
      == x1 Function [Nat,Reals]*)


(* Sequent snapshot:


1:  (Ax2.
     Zero < x2
      & Real(x2)
      & x2 < Sup({x3|Zero < x3 & x3 * x3 < a1})
      -> [a1
      + Minus(Sup({x70|
     Zero < x70 & x70 * x70 < a1})
      * Sup({x71|
     Zero < x71 & x71 * x71 < a1}))]
      * Inv(
     Three
      * Sup({x72|Zero < x72 & x72 * x72 < a1})) <= x2)

2:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

3:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

4:  Real(a1)

5:  Zero < a1

|-

1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

2:  (Ex3.x3 * x3 = a1)


*)



(* 0



-------------------- Not Proved ------------------

Line 1:



|-

1:  (Ax1.Real(x1) & Zero < x1
      -> (Ex2.x2 * x2 = x1))



By 2

-------------------- Not Proved ------------------

Line 2:



|-

1:  Real(a1) & Zero < a1
      -> (Ex3.x3 * x3 = a1)



By 3

-------------------- Not Proved ------------------

Line 3:



1:  Real(a1) & Zero < a1

|-

1:  (Ex3.x3 * x3 = a1)



By 4

-------------------- Not Proved ------------------

Line 4:



1:  Real(a1)

2:  Zero < a1

|-

1:  (Ex3.x3 * x3 = a1)



By 5

-------------------- Not Proved ------------------

Line 5:



1:  Real(a1)

2:  Zero < a1

|-

1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

2:  (Ex3.x3 * x3 = a1)



By 7, 6

-------------------- Not Proved ------------------

Line 7:



1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) Equal a1 v 
     Sup({x3|
     Zero < x3 & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1}) < a1
      v a1 < Sup({x3|Zero < x3 & x3
      * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1})

2:  Real(a1)

3:  Zero < a1

|-

1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

2:  (Ex3.x3 * x3 = a1)



By 9, 8

-------------------- Not Proved ------------------

Line 9:



1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1
      v a1 < Sup({x3|
     Zero < x3 & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1})

2:  Real(a1)

3:  Zero < a1

|-

1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

2:  (Ex3.x3 * x3 = a1)



By 15, 16

-------------------- Not Proved ------------------

Line 15:



1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

2:  Real(a1)

3:  Zero < a1

|-

1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

2:  (Ex3.x3 * x3 = a1)



By 18, 17

-------------------- Not Proved ------------------

Line 18:



1:  (Ax5.
     x5 E {x7|Zero < x7 & x7 * x7 < a1}
      -> x5 <= a1 + One) -> (Ax8.
     x8 E {x10|
     Zero < x10 & x10 * x10 < a1}
      -> x8 <= Sup({x11|Zero < x11 & x11
      * x11 < a1}))

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

3:  Real(a1)

4:  Zero < a1

|-

1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

2:  (Ex3.x3 * x3 = a1)



By 20, 19

-------------------- Not Proved ------------------

Line 20:



1:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

3:  Real(a1)

4:  Zero < a1

|-

1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

2:  (Ex3.x3 * x3 = a1)



By 60, 59

-------------------- Not Proved ------------------

Line 60:



1:  (Ax2.
     Zero < x2
      & Real(x2)
      & x2 < Sup({x3|Zero < x3 & x3 * x3 < a1})
      -> [a1
      + Minus(Sup({x70|
     Zero < x70 & x70 * x70 < a1})
      * Sup({x71|
     Zero < x71 & x71 * x71 < a1}))]
      * Inv(
     Three
      * Sup({x72|Zero < x72 & x72 * x72 < a1})) <= x2)

2:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

3:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

4:  Real(a1)

5:  Zero < a1

|-

1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

2:  (Ex3.x3 * x3 = a1)



-------------------- Proved ----------------------

Line 59:



1:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

3:  Real(a1)

4:  Zero < a1

|-

1:  (Ax2.
     Zero < x2
      & Real(x2)
      & x2 < Sup({x3|Zero < x3 & x3 * x3 < a1})
      -> [a1
      + Minus(Sup({x70|
     Zero < x70 & x70 * x70 < a1})
      * Sup({x71|
     Zero < x71 & x71 * x71 < a1}))]
      * Inv(
     Three
      * Sup({x72|Zero < x72 & x72 * x72 < a1})) <= x2)

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 61

-------------------- Proved ----------------------

Line 61:



1:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

3:  Real(a1)

4:  Zero < a1

|-

1:  
     Zero < a23
      & Real(a23)
      & a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})
      -> [a1
      + Minus(Sup({x71|
     Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))]
      * Inv(
     Three
      * Sup({x73|Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 62

-------------------- Proved ----------------------

Line 62:



1:  Zero < a23
      & Real(a23)
      & a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

2:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

3:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

4:  Real(a1)

5:  Zero < a1

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 63

-------------------- Proved ----------------------

Line 63:



1:  Real(a23)
      & a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

2:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

3:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

4:  Real(a1)

5:  Zero < a1

6:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 64

-------------------- Proved ----------------------

Line 64:



1:  Real(a23)

2:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

3:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

4:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

5:  Real(a1)

6:  Zero < a1

7:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 66, 65

-------------------- Proved ----------------------

Line 66:



1:  Zero < a23
      -> Zero
      + Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x3|
     Zero < x3 & x3 * x3 < a1})

2:  Real(a23)

3:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

4:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

6:  Real(a1)

7:  Zero < a1

8:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 68, 67

-------------------- Proved ----------------------

Line 68:



1:  Zero
      + Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x3|
     Zero < x3 & x3 * x3 < a1})

2:  Real(a23)

3:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

4:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

6:  Real(a1)

7:  Zero < a1

8:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 70, 71, 69

-------------------- Proved ----------------------

Line 70:



1:  Zero
      + Sup({x3|Zero < x3 & x3 * x3 < a1}) = Sup({x3|
     Zero < x3 & x3 * x3 < a1})

2:  Zero
      + Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x3|
     Zero < x3 & x3 * x3 < a1})

3:  Real(a23)

4:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

5:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

7:  Real(a1)

8:  Zero < a1

9:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 72

-------------------- Proved ----------------------

Line 72:



1:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

2:  Real(a23)

3:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

4:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

6:  Real(a1)

7:  Zero < a1

8:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 74, 75, 76, 77, 73

-------------------- Proved ----------------------

Line 74:



1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

2:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

3:  Real(a23)

4:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

5:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

7:  Real(a1)

8:  Zero < a1

9:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 97, 96

-------------------- Proved ----------------------

Line 97:



1:  
     a1 Equal [a23
      + Sup({x3|Zero < x3 & x3 * x3 < a1})] * [
     a23
      + Sup({x3|Zero < x3 & x3 * x3 < a1})]
      v a1 < 
     [a23 + Sup({x3|
     Zero < x3 & x3 * x3 < a1})]
      * [a23 + Sup({x3|Zero < x3 & x3
      * x3 < a1})] v 
     [a23 + Sup({x3|Zero < x3 & x3
      * x3 < a1})]
      * [a23 + Sup({x3|Zero < x3
      & x3 * x3 < a1})] < a1

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

3:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

4:  Real(a23)

5:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

6:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

7:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

8:  Real(a1)

9:  Zero < a1

10:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 99, 98

-------------------- Proved ----------------------

Line 99:



1:  
     a1 < [a23
      + Sup({x3|Zero < x3 & x3 * x3 < a1})] * [
     a23
      + Sup({x3|Zero < x3 & x3 * x3 < a1})] v 
     [a23 + Sup({x3|
     Zero < x3 & x3 * x3 < a1})]
      * [a23 + Sup({x3|Zero < x3 & x3
      * x3 < a1})] < a1

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

3:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

4:  Real(a23)

5:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

6:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

7:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

8:  Real(a1)

9:  Zero < a1

10:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 100, 101

-------------------- Proved ----------------------

Line 100:



1:  a1 < [a23
      + Sup({x3|Zero < x3 & x3 * x3 < a1})] * [
     a23
      + Sup({x3|Zero < x3 & x3 * x3 < a1})]

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

3:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

4:  Real(a23)

5:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

6:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

7:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

8:  Real(a1)

9:  Zero < a1

10:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 261, 260

-------------------- Proved ----------------------

Line 261:



1:  [a23
      + Sup({x4|Zero < x4 & x4 * x4 < a1})] * [
     a23
      + Sup({x5|Zero < x5 & x5 * x5 < a1})] = 
     a23 * a23 + Two
      * a23 * Sup({x6|Zero < x6
      & x6 * x6 < a1})
      + Sup({x7|
     Zero < x7 & x7 * x7 < a1}) * Sup({x8|
     Zero < x8 & x8 * x8 < a1})

2:  a1 < [a23
      + Sup({x3|Zero < x3 & x3 * x3 < a1})] * [
     a23
      + Sup({x3|Zero < x3 & x3 * x3 < a1})]

3:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

4:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

5:  Real(a23)

6:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

7:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

8:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

9:  Real(a1)

10:  Zero < a1

11:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 262

-------------------- Proved ----------------------

Line 262:



1:  a1 < a23 * a23 + Two
      * a23 * Sup({x4|Zero < x4
      & x4 * x4 < a1})
      + Sup({x5|
     Zero < x5 & x5 * x5 < a1}) * Sup({x6|
     Zero < x6 & x6 * x6 < a1})

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

3:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

4:  Real(a23)

5:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

6:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

7:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

8:  Real(a1)

9:  Zero < a1

10:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 264, 265, 266, 263

-------------------- Proved ----------------------

Line 264:



1:  a23 * a23 + Two
      * a23 * Sup({x4|Zero < x4
      & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1}) < 
     a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

2:  a1 < a23 * a23 + Two
      * a23 * Sup({x4|Zero < x4
      & x4 * x4 < a1})
      + Sup({x5|
     Zero < x5 & x5 * x5 < a1}) * Sup({x6|
     Zero < x6 & x6 * x6 < a1})

3:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

4:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

5:  Real(a23)

6:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

7:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

8:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

9:  Real(a1)

10:  Zero < a1

11:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 268, 267

-------------------- Proved ----------------------

Line 268:



1:  
     a1 < a23 * a23 + Two
      * a23 * Sup({x6|Zero < x6
      & x6 * x6 < a1})
      + Sup({x7|
     Zero < x7 & x7 * x7 < a1}) * Sup({x8|
     Zero < x8 & x8 * x8 < a1})
      & a23 * a23
      + 
     
     Two * a23
      * Sup({x9|Zero < x9 & x9 * x9 < a1}) + Sup({x10|
     Zero < x10 & x10 * x10 < a1})
      * Sup({x11|
     Zero < x11 & x11 * x11 < a1}) < 
     a23 * Sup({x4|Zero < x4 & x4
      * x4 < a1}) + Two
      * a23 * Sup({x4|Zero < x4
      & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})
      -> a1 < 
     a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

2:  a23 * a23 + Two
      * a23 * Sup({x4|Zero < x4
      & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1}) < 
     a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

3:  a1 < a23 * a23 + Two
      * a23 * Sup({x4|Zero < x4
      & x4 * x4 < a1})
      + Sup({x5|
     Zero < x5 & x5 * x5 < a1}) * Sup({x6|
     Zero < x6 & x6 * x6 < a1})

4:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

5:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

6:  Real(a23)

7:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

8:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

9:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

10:  Real(a1)

11:  Zero < a1

12:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 270, 269

-------------------- Proved ----------------------

Line 270:



1:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

3:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

4:  Real(a23)

5:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

6:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

7:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

8:  Real(a1)

9:  Zero < a1

10:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 274, 273

-------------------- Proved ----------------------

Line 274:



1:  
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}) < a1 -> 
     Sup({x6|
     Zero < x6 & x6 * x6 < a1}) * Sup({x7|
     Zero < x7 & x7 * x7 < a1})
      + Minus(Sup({x3|Zero < x3
      & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1})) < a1
      + Minus(Sup({x3|Zero < x3
      & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1}))

2:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

3:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

4:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

5:  Real(a23)

6:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

7:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

8:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

9:  Real(a1)

10:  Zero < a1

11:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 276, 275

-------------------- Proved ----------------------

Line 276:



1:  
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1})
      + Minus(Sup({x3|
     Zero < x3 & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1})) < a1
      + Minus(Sup({x3|Zero < x3
      & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1}))

2:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

3:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

4:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

5:  Real(a23)

6:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

7:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

8:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

9:  Real(a1)

10:  Zero < a1

11:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 278, 277

-------------------- Proved ----------------------

Line 278:



1:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1})
      + Minus(Sup({x3|
     Zero < x3 & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1})) = Zero

2:  
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1})
      + Minus(Sup({x3|
     Zero < x3 & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1})) < a1
      + Minus(Sup({x3|Zero < x3
      & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1}))

3:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

4:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

5:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

6:  Real(a23)

7:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

8:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

9:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

10:  Real(a1)

11:  Zero < a1

12:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 279

-------------------- Proved ----------------------

Line 279:



1:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

2:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

3:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

4:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

5:  Real(a23)

6:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

7:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

8:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

9:  Real(a1)

10:  Zero < a1

11:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 281, 280

-------------------- Proved ----------------------

Line 281:



1:  
     a1 < a23
      * Sup({x6|Zero < x6 & x6 * x6 < a1}) + 
     
     Two * a23
      * Sup({x7|Zero < x7 & x7 * x7 < a1})
      + Sup({x8|
     Zero < x8 & x8 * x8 < a1}) * Sup({x9|
     Zero < x9 & x9 * x9 < a1}) -> a1
      + Minus(Sup({x3|Zero < x3
      & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1})) < [a23
      * Sup({x10|Zero < x10 & x10
      * x10 < a1})
      + 
     Two * a23
      * Sup({x11|
     Zero < x11 & x11 * x11 < a1}) + 
     Sup({x12|Zero < x12 & x12
      * x12 < a1}) * Sup({x13|Zero < x13
      & x13 * x13 < a1})]
      + Minus(Sup({x3|
     Zero < x3 & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1}))

2:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

3:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

4:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

5:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

6:  Real(a23)

7:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

8:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

9:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

10:  Real(a1)

11:  Zero < a1

12:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 283, 282

-------------------- Proved ----------------------

Line 283:



1:  a1
      + Minus(
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1})) < 
     [
     a23 * Sup({x6|Zero < x6
      & x6 * x6 < a1}) + Two
      * a23 * Sup({x7|Zero < x7
      & x7 * x7 < a1})
      + Sup({x8|
     Zero < x8 & x8 * x8 < a1}) * Sup({x9|
     Zero < x9 & x9 * x9 < a1})]
      + Minus(Sup({x3|Zero < x3
      & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1}))

2:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

3:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

4:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

5:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

6:  Real(a23)

7:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

8:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

9:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

10:  Real(a1)

11:  Zero < a1

12:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 285, 284

-------------------- Proved ----------------------

Line 285:



1:  [a23
      * Sup({x6|Zero < x6 & x6 * x6 < a1})
      + 
     
     Two * a23
      * Sup({x8|Zero < x8 & x8 * x8 < a1}) + Sup({x9|
     Zero < x9 & x9 * x9 < a1})
      * Sup({x10|
     Zero < x10 & x10 * x10 < a1})]
      + Minus(Sup({x11|
     Zero < x11 & x11 * x11 < a1})
      * Sup({x12|
     Zero < x12 & x12 * x12 < a1})) = 
     a23 * Sup({x6|Zero < x6 & x6
      * x6 < a1}) + 
     [Two
      * a23 * Sup({x13|Zero < x13
      & x13 * x13 < a1}) + Sup({x14|
     Zero < x14 & x14 * x14 < a1})
      * Sup({x15|
     Zero < x15 & x15 * x15 < a1})]
      + Minus(
     Sup({x16|Zero < x16 & x16
      * x16 < a1}) * Sup({x17|Zero < x17
      & x17 * x17 < a1}))

2:  a1
      + Minus(
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1})) < 
     [
     a23 * Sup({x6|Zero < x6
      & x6 * x6 < a1}) + Two
      * a23 * Sup({x7|Zero < x7
      & x7 * x7 < a1})
      + Sup({x8|
     Zero < x8 & x8 * x8 < a1}) * Sup({x9|
     Zero < x9 & x9 * x9 < a1})]
      + Minus(Sup({x3|Zero < x3
      & x3 * x3 < a1}) * Sup({x3|
     Zero < x3 & x3 * x3 < a1}))

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 286

-------------------- Proved ----------------------

Line 286:



1:  a1 + Minus(
     Sup({x11|Zero < x11 & x11 * x11 < a1})
      * Sup({x12|
     Zero < x12 & x12 * x12 < a1})) < 
     a23
      * Sup({x6|Zero < x6 & x6 * x6 < a1}) + 
     [
     Two
      * a23
      * Sup({x13|Zero < x13 & x13 * x13 < a1}) + Sup({x14|
     Zero < x14 & x14 * x14 < a1})
      * Sup({x15|
     Zero < x15 & x15 * x15 < a1})]
      + Minus(
     Sup({x16|Zero < x16 & x16
      * x16 < a1}) * Sup({x17|Zero < x17
      & x17 * x17 < a1}))

2:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

3:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

4:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

5:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

6:  Real(a23)

7:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

8:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

9:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

10:  Real(a1)

11:  Zero < a1

12:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 288, 287

-------------------- Proved ----------------------

Line 288:



1:  
     [Two
      * a23
      * Sup({x13|Zero < x13 & x13 * x13 < a1}) + Sup({x15|
     Zero < x15 & x15 * x15 < a1})
      * Sup({x16|
     Zero < x16 & x16 * x16 < a1})]
      + Minus(
     Sup({x18|Zero < x18 & x18
      * x18 < a1}) * Sup({x19|Zero < x19
      & x19 * x19 < a1})) = Two
      * a23 * Sup({x13|Zero < x13
      & x13 * x13 < a1}) + Sup({x20|
     Zero < x20 & x20 * x20 < a1})
      * Sup({x21|
     Zero < x21 & x21 * x21 < a1})
      + Minus(Sup({x22|
     Zero < x22 & x22 * x22 < a1})
      * Sup({x23|
     Zero < x23 & x23 * x23 < a1}))

2:  a1 + Minus(
     Sup({x11|Zero < x11 & x11 * x11 < a1})
      * Sup({x12|
     Zero < x12 & x12 * x12 < a1})) < 
     a23
      * Sup({x6|Zero < x6 & x6 * x6 < a1}) + 
     [
     Two
      * a23
      * Sup({x13|Zero < x13 & x13 * x13 < a1}) + Sup({x14|
     Zero < x14 & x14 * x14 < a1})
      * Sup({x15|
     Zero < x15 & x15 * x15 < a1})]
      + Minus(
     Sup({x16|Zero < x16 & x16
      * x16 < a1}) * Sup({x17|Zero < x17
      & x17 * x17 < a1}))

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 289

-------------------- Proved ----------------------

Line 289:



1:  a1 + Minus(
     Sup({x20|Zero < x20 & x20 * x20 < a1})
      * Sup({x21|
     Zero < x21 & x21 * x21 < a1})) < 
     a23
      * Sup({x22|Zero < x22 & x22 * x22 < a1})
      + 
     Two
      * a23
      * Sup({x13|Zero < x13 & x13 * x13 < a1}) + Sup({x23|
     Zero < x23 & x23 * x23 < a1})
      * Sup({x24|
     Zero < x24 & x24 * x24 < a1})
      + Minus(Sup({x25|
     Zero < x25 & x25 * x25 < a1})
      * Sup({x26|
     Zero < x26 & x26 * x26 < a1}))

2:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

3:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

4:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

5:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

6:  Real(a23)

7:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

8:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

9:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

10:  Real(a1)

11:  Zero < a1

12:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 291, 290

-------------------- Proved ----------------------

Line 291:



1:  
     Sup({x25|Zero < x25 & x25 * x25 < a1})
      * Sup({x26|
     Zero < x26 & x26 * x26 < a1})
      + Minus(Sup({x25|
     Zero < x25 & x25 * x25 < a1})
      * Sup({x26|
     Zero < x26 & x26 * x26 < a1})) = Zero

2:  a1 + Minus(
     Sup({x20|Zero < x20 & x20 * x20 < a1})
      * Sup({x21|
     Zero < x21 & x21 * x21 < a1})) < 
     a23
      * Sup({x22|Zero < x22 & x22 * x22 < a1})
      + 
     Two
      * a23
      * Sup({x13|Zero < x13 & x13 * x13 < a1}) + Sup({x23|
     Zero < x23 & x23 * x23 < a1})
      * Sup({x24|
     Zero < x24 & x24 * x24 < a1})
      + Minus(Sup({x25|
     Zero < x25 & x25 * x25 < a1})
      * Sup({x26|
     Zero < x26 & x26 * x26 < a1}))

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 292

-------------------- Proved ----------------------

Line 292:



1:  a1 + Minus(
     Sup({x21|Zero < x21 & x21 * x21 < a1})
      * Sup({x22|
     Zero < x22 & x22 * x22 < a1})) < 
     a23
      * Sup({x23|Zero < x23 & x23 * x23 < a1}) + 
     Two
      * a23
      * Sup({x24|Zero < x24 & x24 * x24 < a1})
      + Zero

2:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

3:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

4:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

5:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

6:  Real(a23)

7:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

8:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

9:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

10:  Real(a1)

11:  Zero < a1

12:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 294, 295, 293

-------------------- Proved ----------------------

Line 294:



1:  Two
      * a23
      * Sup({x24|Zero < x24 & x24 * x24 < a1})
      + Zero = Two
      * a23 * Sup({x24|Zero < x24
      & x24 * x24 < a1})

2:  a1 + Minus(
     Sup({x21|Zero < x21 & x21 * x21 < a1})
      * Sup({x22|
     Zero < x22 & x22 * x22 < a1})) < 
     a23
      * Sup({x23|Zero < x23 & x23 * x23 < a1}) + 
     Two
      * a23
      * Sup({x24|Zero < x24 & x24 * x24 < a1})
      + Zero

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 296

-------------------- Proved ----------------------

Line 296:



1:  a1 + Minus(
     Sup({x25|Zero < x25 & x25 * x25 < a1})
      * Sup({x26|
     Zero < x26 & x26 * x26 < a1})) < 
     a23
      * Sup({x27|Zero < x27 & x27 * x27 < a1}) + 
     Two
      * a23
      * Sup({x24|Zero < x24 & x24 * x24 < a1})

2:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

3:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

4:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

5:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

6:  Real(a23)

7:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

8:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

9:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

10:  Real(a1)

11:  Zero < a1

12:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 298, 299, 297

-------------------- Proved ----------------------

Line 298:



1:  a23
      * Sup({x24|Zero < x24 & x24 * x24 < a1}) + 
     Two
      * a23
      * Sup({x24|Zero < x24 & x24 * x24 < a1}) = 
     Three
      * a23
      * Sup({x24|Zero < x24 & x24 * x24 < a1})

2:  a1 + Minus(
     Sup({x25|Zero < x25 & x25 * x25 < a1})
      * Sup({x26|
     Zero < x26 & x26 * x26 < a1})) < 
     a23
      * Sup({x27|Zero < x27 & x27 * x27 < a1}) + 
     Two
      * a23
      * Sup({x24|Zero < x24 & x24 * x24 < a1})

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 300

-------------------- Proved ----------------------

Line 300:



1:  a1 + Minus(
     Sup({x27|Zero < x27 & x27 * x27 < a1})
      * Sup({x28|
     Zero < x28 & x28 * x28 < a1})) < 
     Three
      * a23
      * Sup({x24|Zero < x24 & x24 * x24 < a1})

2:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

3:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

4:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

5:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

6:  Real(a23)

7:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

8:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

9:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

10:  Real(a1)

11:  Zero < a1

12:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 302, 301

-------------------- Proved ----------------------

Line 302:



1:  a23
      * Sup({x25|Zero < x25 & x25 * x25 < a1}) = Sup({x26|
     Zero < x26 & x26 * x26 < a1})
      * a23

2:  a1 + Minus(
     Sup({x27|Zero < x27 & x27 * x27 < a1})
      * Sup({x28|
     Zero < x28 & x28 * x28 < a1})) < 
     Three
      * a23
      * Sup({x24|Zero < x24 & x24 * x24 < a1})

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 303

-------------------- Proved ----------------------

Line 303:



1:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

2:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

3:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

4:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

5:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

6:  Real(a23)

7:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

8:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

9:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

10:  Real(a1)

11:  Zero < a1

12:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 305, 304

-------------------- Proved ----------------------

Line 305:



1:  
     Zero < Inv(Three
      * Sup({x34|Zero < x34 & x34 * x34 < a1}))
      & a1
      + Minus(Sup({x30|
     Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < Three * 
     Sup({x35|Zero < x35 & 
     x35 * x35 < a1}) * a23
      -> 
     [
     a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1}))] * Inv(Three
      * Sup({x36|
     Zero < x36 & x36 * x36 < a1})) < [
     Three
      * 
     Sup({x37|Zero < x37 & x37 * x37 < a1}) * a23]
      * Inv(
     Three
      * Sup({x38|Zero < x38 & x38 * x38 < a1}))

2:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 307, 306

-------------------- Proved ----------------------

Line 307:



1:  
     [a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1}))] * Inv(Three
      * Sup({x34|
     Zero < x34 & x34 * x34 < a1})) < [
     Three
      * 
     Sup({x35|Zero < x35 & x35 * x35 < a1}) * a23]
      * Inv(
     Three
      * Sup({x36|Zero < x36 & x36 * x36 < a1}))

2:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 323, 322

-------------------- Proved ----------------------

Line 323:



1:  
     [Three
      * 
     Sup({x36|Zero < x36 & x36 * x36 < a1}) * a23]
      * Inv(
     Three
      * Sup({x38|Zero < x38 & x38 * x38 < a1})) = 
     Three
      * [
     Sup({x39|Zero < x39 & x39 * x39 < a1}) * a23]
      * Inv(
     Three
      * Sup({x40|Zero < x40 & x40 * x40 < a1}))

2:  
     [a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1}))] * Inv(Three
      * Sup({x34|
     Zero < x34 & x34 * x34 < a1})) < [
     Three
      * 
     Sup({x35|Zero < x35 & x35 * x35 < a1}) * a23]
      * Inv(
     Three
      * Sup({x36|Zero < x36 & x36 * x36 < a1}))

3:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

4:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

5:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

7:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

8:  Real(a23)

9:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

10:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

11:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

12:  Real(a1)

13:  Zero < a1

14:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 324

-------------------- Proved ----------------------

Line 324:



1:  
     [a1 + Minus(
     Sup({x39|Zero < x39 & x39 * x39 < a1})
      * Sup({x40|
     Zero < x40 & x40 * x40 < a1}))] * Inv(Three
      * Sup({x41|
     Zero < x41 & x41 * x41 < a1})) < 
     Three
      * [
     Sup({x42|Zero < x42 & x42 * x42 < a1}) * a23]
      * Inv(
     Three
      * Sup({x43|Zero < x43 & x43 * x43 < a1}))

2:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 326, 325

-------------------- Proved ----------------------

Line 326:



1:  [
     Sup({x42|Zero < x42 & x42 * x42 < a1}) * a23]
      * Inv(
     Three
      * Sup({x45|Zero < x45 & x45 * x45 < a1})) = Sup({x42|
     Zero < x42 & x42 * x42 < a1}) * 
     a23
      * Inv(Three
      * Sup({x46|Zero < x46 & x46 * x46 < a1}))

2:  
     [a1 + Minus(
     Sup({x39|Zero < x39 & x39 * x39 < a1})
      * Sup({x40|
     Zero < x40 & x40 * x40 < a1}))] * Inv(Three
      * Sup({x41|
     Zero < x41 & x41 * x41 < a1})) < 
     Three
      * [
     Sup({x42|Zero < x42 & x42 * x42 < a1}) * a23]
      * Inv(
     Three
      * Sup({x43|Zero < x43 & x43 * x43 < a1}))

3:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

4:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

5:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

7:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

8:  Real(a23)

9:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

10:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

11:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

12:  Real(a1)

13:  Zero < a1

14:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 327

-------------------- Proved ----------------------

Line 327:



1:  
     [a1 + Minus(
     Sup({x46|Zero < x46 & x46 * x46 < a1})
      * Sup({x47|
     Zero < x47 & x47 * x47 < a1}))] * Inv(Three
      * Sup({x48|
     Zero < x48 & x48 * x48 < a1})) < 
     Three * 
     Sup({x42|Zero < x42 & x42 * x42 < a1})
      * a23
      * Inv(
     Three
      * Sup({x49|Zero < x49 & x49 * x49 < a1}))

2:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 329, 328

-------------------- Proved ----------------------

Line 329:



1:  a23
      * Inv(Three
      * Sup({x50|Zero < x50 & x50 * x50 < a1})) = Inv(
     Three
      * Sup({x51|Zero < x51 & x51 * x51 < a1}))
      * a23

2:  
     [a1 + Minus(
     Sup({x46|Zero < x46 & x46 * x46 < a1})
      * Sup({x47|
     Zero < x47 & x47 * x47 < a1}))] * Inv(Three
      * Sup({x48|
     Zero < x48 & x48 * x48 < a1})) < 
     Three * 
     Sup({x42|Zero < x42 & x42 * x42 < a1})
      * a23
      * Inv(
     Three
      * Sup({x49|Zero < x49 & x49 * x49 < a1}))

3:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

4:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

5:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

7:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

8:  Real(a23)

9:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

10:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

11:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

12:  Real(a1)

13:  Zero < a1

14:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 330

-------------------- Proved ----------------------

Line 330:



1:  
     [a1 + Minus(
     Sup({x51|Zero < x51 & x51 * x51 < a1})
      * Sup({x52|
     Zero < x52 & x52 * x52 < a1}))] * Inv(Three
      * Sup({x53|
     Zero < x53 & x53 * x53 < a1})) < 
     Three * 
     Sup({x54|Zero < x54 & x54 * x54 < a1}) * Inv(Three
      * Sup({x55|
     Zero < x55 & x55 * x55 < a1}))
      * a23

2:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 332, 331

-------------------- Proved ----------------------

Line 332:



1:  
     [Three
      * Sup({x55|Zero < x55 & x55 * x55 < a1})] * Inv(
     Three
      * Sup({x57|Zero < x57 & x57 * x57 < a1}))
      * a23 = Three * Sup({x58|Zero < x58
      & x58 * x58 < a1}) * Inv(
     Three
      * Sup({x59|Zero < x59 & x59 * x59 < a1}))
      * a23

2:  
     [a1 + Minus(
     Sup({x51|Zero < x51 & x51 * x51 < a1})
      * Sup({x52|
     Zero < x52 & x52 * x52 < a1}))] * Inv(Three
      * Sup({x53|
     Zero < x53 & x53 * x53 < a1})) < 
     Three * 
     Sup({x54|Zero < x54 & x54 * x54 < a1}) * Inv(Three
      * Sup({x55|
     Zero < x55 & x55 * x55 < a1}))
      * a23

3:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

4:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

5:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

7:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

8:  Real(a23)

9:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

10:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

11:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

12:  Real(a1)

13:  Zero < a1

14:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 333

-------------------- Proved ----------------------

Line 333:



1:  
     [a1 + Minus(
     Sup({x58|Zero < x58 & x58 * x58 < a1})
      * Sup({x59|
     Zero < x59 & x59 * x59 < a1}))] * Inv(Three
      * Sup({x60|
     Zero < x60 & x60 * x60 < a1})) < [
     Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})] * Inv(
     Three
      * Sup({x62|Zero < x62 & x62 * x62 < a1}))
      * a23

2:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 335, 334

-------------------- Proved ----------------------

Line 335:



1:  [
     [Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})]
      * Inv(
     Three
      * Sup({x63|Zero < x63 & x63 * x63 < a1}))]
      * a23 = 
     [Three * Sup({x61|Zero < x61
      & x61 * x61 < a1})] * 
     Inv(Three * Sup({x64|Zero < x64
      & x64 * x64 < a1})) * a23

2:  
     [a1 + Minus(
     Sup({x58|Zero < x58 & x58 * x58 < a1})
      * Sup({x59|
     Zero < x59 & x59 * x59 < a1}))] * Inv(Three
      * Sup({x60|
     Zero < x60 & x60 * x60 < a1})) < [
     Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})] * Inv(
     Three
      * Sup({x62|Zero < x62 & x62 * x62 < a1}))
      * a23

3:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

4:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

5:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

7:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

8:  Real(a23)

9:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

10:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

11:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

12:  Real(a1)

13:  Zero < a1

14:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 336

-------------------- Proved ----------------------

Line 336:



1:  
     [a1 + Minus(
     Sup({x64|Zero < x64 & x64 * x64 < a1})
      * Sup({x65|
     Zero < x65 & x65 * x65 < a1}))] * Inv(Three
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1})) < [[
     Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})]
      * Inv(
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}))]
      * a23

2:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 338, 337

-------------------- Proved ----------------------

Line 338:



1:  
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}) Equal Zero
      v [
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1})]
      * Inv(
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1})) = One

2:  
     [a1 + Minus(
     Sup({x64|Zero < x64 & x64 * x64 < a1})
      * Sup({x65|
     Zero < x65 & x65 * x65 < a1}))] * Inv(Three
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1})) < [[
     Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})]
      * Inv(
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}))]
      * a23

3:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

4:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

5:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

7:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

8:  Real(a23)

9:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

10:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

11:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

12:  Real(a1)

13:  Zero < a1

14:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 339, 340

-------------------- Proved ----------------------

Line 339:



1:  Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}) Equal Zero

2:  
     [a1 + Minus(
     Sup({x64|Zero < x64 & x64 * x64 < a1})
      * Sup({x65|
     Zero < x65 & x65 * x65 < a1}))] * Inv(Three
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1})) < [[
     Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})]
      * Inv(
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}))]
      * a23

3:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

4:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

5:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

7:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

8:  Real(a23)

9:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

10:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

11:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

12:  Real(a1)

13:  Zero < a1

14:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 353, 354, 355, 356, 352

-------------------- Proved ----------------------

Line 353:



1:  Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}) = Zero

2:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

14:  
     [a1 + Minus(
     Sup({x64|Zero < x64 & x64 * x64 < a1})
      * Sup({x65|
     Zero < x65 & x65 * x65 < a1}))] * Inv(Three
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1})) < [[
     Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})]
      * Inv(
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}))]
      * a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 358, 357

-------------------- Proved ----------------------

Line 358:



1:  
     [Three
      * Sup({x33|Zero < x33 & x33 * x33 < a1})]
      * a23 = Three * Sup({x34|Zero < x34
      & x34 * x34 < a1})
      * a23

2:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

14:  
     [a1 + Minus(
     Sup({x64|Zero < x64 & x64 * x64 < a1})
      * Sup({x65|
     Zero < x65 & x65 * x65 < a1}))] * Inv(Three
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1})) < [[
     Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})]
      * Inv(
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}))]
      * a23

15:  Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}) = Zero

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 359

-------------------- Proved ----------------------

Line 359:



1:  Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}) = Zero

2:  a1 + Minus(
     Sup({x34|Zero < x34 & x34 * x34 < a1})
      * Sup({x35|
     Zero < x35 & x35 * x35 < a1})) < [
     Three
      * Sup({x36|Zero < x36 & x36 * x36 < a1})]
      * a23

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

14:  
     [a1 + Minus(
     Sup({x64|Zero < x64 & x64 * x64 < a1})
      * Sup({x65|
     Zero < x65 & x65 * x65 < a1}))] * Inv(Three
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1})) < [[
     Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})]
      * Inv(
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}))]
      * a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 360

-------------------- Proved ----------------------

Line 360:



1:  a1 + Minus(
     Sup({x35|Zero < x35 & x35 * x35 < a1})
      * Sup({x36|
     Zero < x36 & x36 * x36 < a1})) < 
     Zero * a23

2:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

3:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

4:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

5:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

6:  Real(a23)

7:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

8:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

9:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

10:  Real(a1)

11:  Zero < a1

12:  Zero < a23

13:  
     [a1 + Minus(
     Sup({x64|Zero < x64 & x64 * x64 < a1})
      * Sup({x65|
     Zero < x65 & x65 * x65 < a1}))] * Inv(Three
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1})) < [[
     Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})]
      * Inv(
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}))]
      * a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 362, 361

-------------------- Proved ----------------------

Line 362:



1:  Zero * a23 = Zero

2:  a1 + Minus(
     Sup({x35|Zero < x35 & x35 * x35 < a1})
      * Sup({x36|
     Zero < x36 & x36 * x36 < a1})) < 
     Zero * a23

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

14:  
     [a1 + Minus(
     Sup({x64|Zero < x64 & x64 * x64 < a1})
      * Sup({x65|
     Zero < x65 & x65 * x65 < a1}))] * Inv(Three
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1})) < [[
     Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})]
      * Inv(
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}))]
      * a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 363

-------------------- Proved ----------------------

Line 363:



1:  a1 + Minus(
     Sup({x36|Zero < x36 & x36 * x36 < a1})
      * Sup({x37|
     Zero < x37 & x37 * x37 < a1})) < Zero

2:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

|-


By NOTBOTH

Proof of NOTBOTH begins



-------------------- Proved ----------------------

Line 46.3:



1:  a2 < a1

2:  a1 < a2

|-



By 4, 5

-------------------- Proved ----------------------

Line 46.4:



|-

1:  a2 < a1 & a1 < a2 -> a2 < a2


By NOTBOTH.TRANS

Proof of NOTBOTH.TRANS begins



-------------------- Proved ----------------------

Line 19.19:



|-

1:  a1 < a2 & a2 < a3 -> a1 < a3


By NOTBOTH.TRANS.TRANSTheorem reference error

Proof of NOTBOTH.TRANS ends



-------------------- Proved ----------------------

Line 46.5:



1:  a2 < a1 & a1 < a2 -> a2 < a2

2:  a2 < a1

3:  a1 < a2

|-



By 6, 7

-------------------- Proved ----------------------

Line 46.6:



1:  a2 < a1

2:  a1 < a2

|-

1:  a2 < a1 & a1 < a2



By 8, 9

-------------------- Trivial ---------------------

Line 46.8:



1:  a2 < a1

|-

1:  a2 < a1



-------------------- Trivial ---------------------

Line 46.9:



1:  a1 < a2

|-

1:  a1 < a2



-------------------- Proved ----------------------

Line 46.7:



1:  a2 < a2

|-



By 10, 11

-------------------- Proved ----------------------

Line 46.10:



|-

1:  ~a2 < a2


By NOTBOTH.IRR

Proof of NOTBOTH.IRR begins



-------------------- Proved ----------------------

Line 17.17:



|-

1:  ~a1 < a1


By NOTBOTH.IRR.IRRTheorem reference error

Proof of NOTBOTH.IRR ends



-------------------- Proved ----------------------

Line 46.11:



1:  ~a2 < a2

2:  a2 < a2

|-



By 12

-------------------- Trivial ---------------------

Line 46.12:



1:  a2 < a2

|-

1:  a2 < a2



Proof of NOTBOTH ends



-------------------- Proved ----------------------

Line 361:



|-

1:  Zero * a23 = Zero


By MZERO2

Proof of MZERO2 begins



-------------------- Proved ----------------------

Line 43.1:



|-

1:  Zero * a1 = Zero



By 2, 3

-------------------- Proved ----------------------

Line 43.2:



|-

1:  Zero * a1 = a1 * Zero


By MZERO2.CTIMES

Proof of MZERO2.CTIMES begins



-------------------- Proved ----------------------

Line 8.8:



|-

1:  a1 * a2 = a2 * a1


By MZERO2.CTIMES.CTIMESTheorem reference error

Proof of MZERO2.CTIMES ends



-------------------- Proved ----------------------

Line 43.3:



1:  Zero * a1 = a1 * Zero

|-

1:  Zero * a1 = Zero



By 4

-------------------- Proved ----------------------

Line 43.4:



|-

1:  a1 * Zero = Zero


By MZERO2.MZERO

Proof of MZERO2.MZERO begins



-------------------- Proved ----------------------

Line 30.1:



|-

1:  a1 * Zero = Zero



By 2, 3

-------------------- Proved ----------------------

Line 30.2:



1:  a1 * Zero + a1 * Zero = a1 * Zero

|-

1:  a1 * Zero = Zero



By 4, 5, 6, 7

-------------------- Proved ----------------------

Line 30.4:



1:  Real(a1 * Zero)

2:  Real(a1 * Zero)

|-

1:  
     a1 * Zero + a1 * Zero = a1 * Zero
      == a1 * Zero = Zero


By MZERO2.MZERO.NULLADD

Proof of MZERO2.MZERO.NULLADD begins



-------------------- Proved ----------------------

Line 25.3:



1:  Real(a1)

2:  Real(a2)

|-

1:  a1 + a2 = a1 == a2 = Zero



By 4

-------------------- Proved ----------------------

Line 25.4:



1:  Real(a1)

2:  Real(a2)

|-

1:  
     (a1 + a2 = a1 -> a2 = Zero) & (a2 = Zero
      -> a1 + a2 = a1)



By 5, 6

-------------------- Proved ----------------------

Line 25.5:



1:  Real(a2)

|-

1:  a1 + a2 = a1 -> a2 = Zero



By 7

-------------------- Proved ----------------------

Line 25.7:



1:  a1 + a2 = a1

2:  Real(a2)

|-

1:  a2 = Zero



By 8, 9

-------------------- Proved ----------------------

Line 25.8:



1:  a1 + a2 = a1

|-

1:  [a1 + a2] + Minus(a1) = a1 + Minus(a1)



By 10

-------------------- Trivial ---------------------

Line 25.10:



|-

1:  a1 + Minus(a1) = a1 + Minus(a1)



-------------------- Proved ----------------------

Line 25.9:



1:  [a1 + a2] + Minus(a1) = a1 + Minus(a1)

2:  Real(a2)

|-

1:  a2 = Zero



By 11, 12

-------------------- Proved ----------------------

Line 25.11:



|-

1:  a1 + Minus(a1) = Zero


By MZERO2.MZERO.NULLADD.MINUS

Proof of MZERO2.MZERO.NULLADD.MINUS begins



-------------------- Proved ----------------------

Line 14.14:



|-

1:  a1 + Minus(a1) = Zero


By MZERO2.MZERO.NULLADD.MINUS.MINUSTheorem reference error

Proof of MZERO2.MZERO.NULLADD.MINUS ends



-------------------- Proved ----------------------

Line 25.12:



1:  [a1 + a2] + Minus(a1) = a1 + Minus(a1)

2:  a1 + Minus(a1) = Zero

3:  Real(a2)

|-

1:  a2 = Zero



By 13

-------------------- Proved ----------------------

Line 25.13:



1:  [a1 + a2] + Minus(a1) = Zero

2:  a1 + Minus(a1) = Zero

3:  Real(a2)

|-

1:  a2 = Zero



By 14, 15

-------------------- Proved ----------------------

Line 25.14:



1:  [a1 + a2] + Minus(a1) = Zero

2:  [a1 + a2] + Minus(a1) = a2

|-

1:  a2 = Zero



By 16

-------------------- Trivial ---------------------

Line 25.16:



1:  a2 = Zero

|-

1:  a2 = Zero



-------------------- Proved ----------------------

Line 25.15:



1:  a1 + Minus(a1) = Zero

2:  Real(a2)

|-

1:  [a1 + a2] + Minus(a1) = a2



By 17, 18

-------------------- Proved ----------------------

Line 25.17:



|-

1:  a1 + a2 = a2 + a1


By MZERO2.MZERO.NULLADD.CPLUS

Proof of MZERO2.MZERO.NULLADD.CPLUS begins



-------------------- Proved ----------------------

Line 7.7:



|-

1:  a1 + a2 = a2 + a1


By MZERO2.MZERO.NULLADD.CPLUS.CPLUSTheorem reference error

Proof of MZERO2.MZERO.NULLADD.CPLUS ends



-------------------- Proved ----------------------

Line 25.18:



1:  a1 + a2 = a2 + a1

2:  a1 + Minus(a1) = Zero

3:  Real(a2)

|-

1:  [a1 + a2] + Minus(a1) = a2



By 19

-------------------- Proved ----------------------

Line 25.19:



1:  a1 + a2 = a2 + a1

2:  a1 + Minus(a1) = Zero

3:  Real(a2)

|-

1:  [a1 + a2] + Minus(a1) = a2



By 20, 21

-------------------- Proved ----------------------

Line 25.20:



|-

1:  [a2 + a1] + Minus(a1) = a2
      + a1 + Minus(a1)


By MZERO2.MZERO.NULLADD.APLUS

Proof of MZERO2.MZERO.NULLADD.APLUS begins



-------------------- Proved ----------------------

Line 9.9:



|-

1:  [a1 + a2] + a3 = a1 + a2 + a3


By MZERO2.MZERO.NULLADD.APLUS.APLUSTheorem reference error

Proof of MZERO2.MZERO.NULLADD.APLUS ends



-------------------- Proved ----------------------

Line 25.21:



1:  [a2 + a1] + Minus(a1) = a2
      + a1 + Minus(a1)

2:  a1 + Minus(a1) = Zero

3:  Real(a2)

4:  a1 + a2 = a2 + a1

|-

1:  [a1 + a2] + Minus(a1) = a2



By 22

-------------------- Proved ----------------------

Line 25.22:



1:  [a2 + a1] + Minus(a1) = a2 + Zero

2:  Real(a2)

3:  a1 + a2 = a2 + a1

|-

1:  [a1 + a2] + Minus(a1) = a2



By 23, 24

-------------------- Proved ----------------------

Line 25.23:



|-

1:  Real(a2) -> a2 + Zero = a2


By MZERO2.MZERO.NULLADD.IPLUS

Proof of MZERO2.MZERO.NULLADD.IPLUS begins



-------------------- Proved ----------------------

Line 12.12:



|-

1:  Real(a1) -> a1 + Zero = a1


By MZERO2.MZERO.NULLADD.IPLUS.IPLUSTheorem reference error

Proof of MZERO2.MZERO.NULLADD.IPLUS ends



-------------------- Proved ----------------------

Line 25.24:



1:  Real(a2) -> a2 + Zero = a2

2:  [a2 + a1] + Minus(a1) = a2 + Zero

3:  Real(a2)

4:  a1 + a2 = a2 + a1

|-

1:  [a1 + a2] + Minus(a1) = a2



By 25, 26

-------------------- Trivial ---------------------

Line 25.25:



1:  Real(a2)

|-

1:  Real(a2)



-------------------- Proved ----------------------

Line 25.26:



1:  [a2 + a1] + Minus(a1) = a2 + Zero

2:  a2 + Zero = a2

3:  a1 + a2 = a2 + a1

|-

1:  [a1 + a2] + Minus(a1) = a2



By 27

-------------------- Proved ----------------------

Line 25.27:



1:  [a2 + a1] + Minus(a1) = a2 + Zero

2:  a2 + Zero = a2

3:  a1 + a2 = a2 + a1

|-

1:  [a1 + a2] + Minus(a1) = a2



By 28

-------------------- Proved ----------------------

Line 25.28:



1:  a1 + a2 = a2 + a1

2:  [a2 + a1] + Minus(a1) = a2

|-

1:  [a1 + a2] + Minus(a1) = a2



By 29

-------------------- Trivial ---------------------

Line 25.29:



1:  [a2 + a1] + Minus(a1) = a2

|-

1:  [a2 + a1] + Minus(a1) = a2



-------------------- Proved ----------------------

Line 25.6:



1:  Real(a1)

|-

1:  a2 = Zero -> a1 + a2 = a1



By 30

-------------------- Proved ----------------------

Line 25.30:



1:  a2 = Zero

2:  Real(a1)

|-

1:  a1 + a2 = a1



By 31

-------------------- Proved ----------------------

Line 25.31:



1:  Real(a1)

|-

1:  a1 + Zero = a1



By 32, 33

-------------------- Proved ----------------------

Line 25.32:



|-

1:  Real(a1) -> a1 + Zero = a1


By MZERO2.MZERO.NULLADD.IPLUSAlready shown (12)

-------------------- Proved ----------------------

Line 25.33:



1:  Real(a1) -> a1 + Zero = a1

2:  Real(a1)

|-

1:  a1 + Zero = a1



By 35, 36

-------------------- Trivial ---------------------

Line 25.35:



1:  Real(a1)

|-

1:  Real(a1)



-------------------- Trivial ---------------------

Line 25.36:



1:  a1 + Zero = a1

|-

1:  a1 + Zero = a1



Proof of MZERO2.MZERO.NULLADD ends



-------------------- Proved ----------------------

Line 30.5:



1:  
     a1 * Zero + a1 * Zero = a1 * Zero
      == a1 * Zero = Zero

2:  a1 * Zero + a1 * Zero = a1 * Zero

|-

1:  a1 * Zero = Zero



By 8

-------------------- Proved ----------------------

Line 30.8:



1:  (
     a1 * Zero + a1 * Zero = a1 * Zero
      -> a1 * Zero = Zero)
      & (
     a1 * Zero = Zero -> 
     a1 * Zero + a1 * Zero = a1 * Zero)

2:  a1 * Zero + a1 * Zero = a1 * Zero

|-

1:  a1 * Zero = Zero



By 9

-------------------- Proved ----------------------

Line 30.9:



1:  
     a1 * Zero + a1 * Zero = a1 * Zero
      -> a1 * Zero = Zero

2:  a1 * Zero + a1 * Zero = a1 * Zero

|-

1:  a1 * Zero = Zero


By MZERO2.MZERO.MP

Proof of MZERO2.MZERO.MP begins



-------------------- Proved ----------------------

Line 28.1:



1:  P1 -> P2

2:  P1

|-

1:  P2



By 2, 3

-------------------- Trivial ---------------------

Line 28.2:



1:  P1

|-

1:  P1



-------------------- Trivial ---------------------

Line 28.3:



1:  P2

|-

1:  P2



Proof of MZERO2.MZERO.MP ends



-------------------- Proved ----------------------

Line 30.6:



|-

1:  Real(a1 * Zero)


By MZERO2.MZERO.RTIMES

Proof of MZERO2.MZERO.RTIMES begins



-------------------- Proved ----------------------

Line 3.3:



|-

1:  Real(a1 * a2)


By MZERO2.MZERO.RTIMES.RTIMESTheorem reference error

Proof of MZERO2.MZERO.RTIMES ends



-------------------- Proved ----------------------

Line 30.7:



|-

1:  Real(a1 * Zero)


By MZERO2.MZERO.RTIMESAlready shown (3)

-------------------- Proved ----------------------

Line 30.3:



|-

1:  a1 * Zero + a1 * Zero = a1 * Zero



By 10, 11

-------------------- Proved ----------------------

Line 30.10:



|-

1:  a1 * [Zero + Zero] = a1 * Zero + a1
      * Zero


By MZERO2.MZERO.DIST

Proof of MZERO2.MZERO.DIST begins



-------------------- Proved ----------------------

Line 11.11:



|-

1:  a1 * [a2 + a3] = a1 * a2
      + a1 * a3


By MZERO2.MZERO.DIST.DISTTheorem reference error

Proof of MZERO2.MZERO.DIST ends



-------------------- Proved ----------------------

Line 30.11:



1:  a1 * [Zero + Zero] = a1 * Zero + a1
      * Zero

|-

1:  a1 * Zero + a1 * Zero = a1 * Zero



By 12

-------------------- Proved ----------------------

Line 30.12:



|-

1:  a1 * [Zero + Zero] = a1 * Zero



By 13, 14

-------------------- Proved ----------------------

Line 30.13:



|-

1:  Real(Zero) -> Zero + Zero = Zero


By MZERO2.MZERO.IPLUSAlready shown (12)

-------------------- Proved ----------------------

Line 30.14:



1:  Real(Zero) -> Zero + Zero = Zero

|-

1:  a1 * [Zero + Zero] = a1 * Zero



By 15, 16

-------------------- Proved ----------------------

Line 30.15:



|-

1:  Real(Zero)


By MZERO2.MZERO.RZERO

Proof of MZERO2.MZERO.RZERO begins



-------------------- Proved ----------------------

Line 29.1:



|-

1:  Real(Zero)



By 2, 3

-------------------- Proved ----------------------

Line 29.2:



|-

1:  U1 + Minus(U1) = Zero


By MZERO2.MZERO.RZERO.MINUSAlready shown (14)

-------------------- Proved ----------------------

Line 29.3:



1:  U1 + Minus(U1) = Zero

|-

1:  Real(Zero)



By 4

-------------------- Proved ----------------------

Line 29.4:



|-

1:  Real(U1 + Minus(U1))


By MZERO2.MZERO.RZERO.RPLUS

Proof of MZERO2.MZERO.RZERO.RPLUS begins



-------------------- Proved ----------------------

Line 2.2:



|-

1:  Real(a1 + a2)


By MZERO2.MZERO.RZERO.RPLUS.RPLUSTheorem reference error

Proof of MZERO2.MZERO.RZERO.RPLUS ends



Proof of MZERO2.MZERO.RZERO ends



-------------------- Proved ----------------------

Line 30.16:



1:  Zero + Zero = Zero

|-

1:  a1 * [Zero + Zero] = a1 * Zero



By 17

-------------------- Trivial ---------------------

Line 30.17:



|-

1:  a1 * Zero = a1 * Zero



Proof of MZERO2.MZERO ends



Proof of MZERO2 ends



-------------------- Proved ----------------------

Line 357:



|-

1:  
     [Three
      * Sup({x33|Zero < x33 & x33 * x33 < a1})]
      * a23 = Three * Sup({x34|Zero < x34
      & x34 * x34 < a1})
      * a23


By ATIMES

Proof of ATIMES begins



-------------------- Proved ----------------------

Line 10.10:



|-

1:  [a1 * a2] * a3 = a1 * a2 * a3


By ATIMES.ATIMESTheorem reference error

Proof of ATIMES ends



-------------------- Trivial ---------------------

Line 354:



1:  Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}) Equal Zero

2:  
     [a1 + Minus(
     Sup({x64|Zero < x64 & x64 * x64 < a1})
      * Sup({x65|
     Zero < x65 & x65 * x65 < a1}))] * Inv(Three
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1})) < [[
     Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})]
      * Inv(
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}))]
      * a23

3:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

4:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

5:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

7:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

8:  Real(a23)

9:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

10:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

11:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

12:  Real(a1)

13:  Zero < a1

14:  Zero < a23

|-

1:  Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}) Equal Zero

2:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

3:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

4:  (Ex3.x3 * x3 = a1)



-------------------- Proved ----------------------

Line 355:



|-

1:  Real(Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}))


By RTIMESAlready shown (3)

-------------------- Proved ----------------------

Line 356:



|-

1:  Real(Zero)


By RZEROAlready shown (29)

-------------------- Proved ----------------------

Line 352:



1:  Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}) Equal Zero

2:  Real(Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}))

3:  Real(Zero)

|-

1:  Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}) = Zero


By EQUALITY

Proof of EQUALITY begins



-------------------- Proved ----------------------

Line 36.4:



1:  a1 Equal a2

2:  Real(a1)

3:  Real(a2)

|-

1:  a1 = a2



By 5

-------------------- Proved ----------------------

Line 36.5:



1:  a1 + Zero = a2 + Zero

2:  Real(a1)

3:  Real(a2)

|-

1:  a1 = a2



By 6, 7

-------------------- Proved ----------------------

Line 36.6:



|-

1:  Real(a1) -> a1 + Zero = a1


By EQUALITY.IPLUSAlready shown (12)

-------------------- Proved ----------------------

Line 36.7:



1:  Real(a1) -> a1 + Zero = a1

2:  a1 + Zero = a2 + Zero

3:  Real(a1)

4:  Real(a2)

|-

1:  a1 = a2



By 8, 9

-------------------- Trivial ---------------------

Line 36.8:



1:  Real(a1)

|-

1:  Real(a1)



-------------------- Proved ----------------------

Line 36.9:



1:  a1 + Zero = a1

2:  a1 + Zero = a2 + Zero

3:  Real(a2)

|-

1:  a1 = a2



By 10

-------------------- Proved ----------------------

Line 36.10:



1:  a1 + Zero = a1

2:  a1 = a2 + Zero

3:  Real(a2)

|-

1:  a1 = a2



By 11, 12

-------------------- Proved ----------------------

Line 36.11:



|-

1:  Real(a2) -> a2 + Zero = a2


By EQUALITY.IPLUSAlready shown (12)

-------------------- Proved ----------------------

Line 36.12:



1:  Real(a2) -> a2 + Zero = a2

2:  a1 + Zero = a1

3:  a1 = a2 + Zero

4:  Real(a2)

|-

1:  a1 = a2



By 13, 14

-------------------- Trivial ---------------------

Line 36.13:



1:  Real(a2)

|-

1:  Real(a2)



-------------------- Proved ----------------------

Line 36.14:



1:  a2 + Zero = a2

2:  a1 = a2 + Zero

3:  a1 + Zero = a1

|-

1:  a1 = a2



By 15

-------------------- Trivial ---------------------

Line 36.15:



1:  a1 = a2

2:  a1 + Zero = a1

3:  a2 + Zero = a2

|-

1:  a1 = a2



Proof of EQUALITY ends



-------------------- Proved ----------------------

Line 340:



1:  
     [Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1})]
      * Inv(
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1})) = One

2:  
     [a1 + Minus(
     Sup({x64|Zero < x64 & x64 * x64 < a1})
      * Sup({x65|
     Zero < x65 & x65 * x65 < a1}))] * Inv(Three
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1})) < [[
     Three
      * Sup({x61|Zero < x61 & x61 * x61 < a1})]
      * Inv(
     Three
      * Sup({x67|Zero < x67 & x67 * x67 < a1}))]
      * a23

3:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

4:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

5:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

7:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

8:  Real(a23)

9:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

10:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

11:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

12:  Real(a1)

13:  Zero < a1

14:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 341

-------------------- Proved ----------------------

Line 341:



1:  
     [a1 + Minus(
     Sup({x65|Zero < x65 & x65 * x65 < a1})
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1}))] * Inv(Three
      * Sup({x67|
     Zero < x67 & x67 * x67 < a1})) < 
     One * a23

2:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

3:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

4:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

5:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

6:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

7:  Real(a23)

8:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

9:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

10:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

11:  Real(a1)

12:  Zero < a1

13:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 343, 342

-------------------- Proved ----------------------

Line 343:



1:  Real(a23) -> a23 * One = a23

2:  
     [a1 + Minus(
     Sup({x65|Zero < x65 & x65 * x65 < a1})
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1}))] * Inv(Three
      * Sup({x67|
     Zero < x67 & x67 * x67 < a1})) < 
     One * a23

3:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

4:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

5:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

7:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

8:  Real(a23)

9:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

10:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

11:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

12:  Real(a1)

13:  Zero < a1

14:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 345, 344

-------------------- Proved ----------------------

Line 345:



1:  a23 * One = One * a23

2:  Real(a23) -> a23 * One = a23

3:  
     [a1 + Minus(
     Sup({x65|Zero < x65 & x65 * x65 < a1})
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1}))] * Inv(Three
      * Sup({x67|
     Zero < x67 & x67 * x67 < a1})) < 
     One * a23

4:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

5:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

6:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

7:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

8:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

9:  Real(a23)

10:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

11:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

12:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

13:  Real(a1)

14:  Zero < a1

15:  Zero < a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 346

-------------------- Proved ----------------------

Line 346:



1:  Real(a23) -> One * a23 = a23

2:  
     [a1 + Minus(
     Sup({x65|Zero < x65 & x65 * x65 < a1})
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1}))] * Inv(Three
      * Sup({x67|
     Zero < x67 & x67 * x67 < a1})) < 
     One * a23

3:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

4:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

5:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

7:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

8:  Real(a23)

9:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

10:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

11:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

12:  Real(a1)

13:  Zero < a1

14:  Zero < a23

15:  a23 * One = One * a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 348, 347

-------------------- Proved ----------------------

Line 348:



1:  One * a23 = a23

2:  
     [a1 + Minus(
     Sup({x65|Zero < x65 & x65 * x65 < a1})
      * Sup({x66|
     Zero < x66 & x66 * x66 < a1}))] * Inv(Three
      * Sup({x67|
     Zero < x67 & x67 * x67 < a1})) < 
     One * a23

3:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      * 
     Sup({x32|Zero < x32 & x32 * x32 < a1}) * a23

4:  Zero < a1
      + Minus(
     Sup({x4|Zero < x4 & x4 * x4 < a1}) * Sup({x5|Zero < x5 & x5
      * x5 < a1}))

5:  a1 < a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1}) + 
     
     Two * a23
      * Sup({x4|Zero < x4 & x4 * x4 < a1})
      + Sup({x4|
     Zero < x4 & x4 * x4 < a1}) * Sup({x4|
     Zero < x4 & x4 * x4 < a1})

6:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < 
     [a23 + Sup({x6|
     Zero < x6 & x6 * x6 < a1})]
      * [a23 + Sup({x7|Zero < x7 & x7
      * x7 < a1})]

7:  Sup({x3|Zero < x3 & x3 * x3 < a1}) < a23 + Sup({x5|Zero < x5
      & x5 * x5 < a1})

8:  Real(a23)

9:  a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})

10:  (Ax4.
     x4 E {x3|Zero < x3 & x3 * x3 < a1}
      -> x4 <= Sup({x3|Zero < x3 & x3
      * x3 < a1}))

11:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) < a1

12:  Real(a1)

13:  Zero < a1

14:  Zero < a23

15:  a23 * One = One * a23

|-

1:  
     [a1 + Minus(
     Sup({x71|Zero < x71 & x71 * x71 < a1})
      * Sup({x72|
     Zero < x72 & x72 * x72 < a1}))] * Inv(Three
      * Sup({x73|
     Zero < x73 & x73 * x73 < a1})) <= a23

2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1

3:  (Ex3.x3 * x3 = a1)



By 349

-------------------- Proved ----------------------

Line 349:



1:  
     [a1 + Minus(
     Sup({x66|Zero < x66 & x66 * x66 < a1})
      * Sup({x67|
     Zero < x67 & x67 * x67 < a1}))] * Inv(Three
      * Sup({x68|
     Zero < x68 & x68 * x68 < a1})) < a23

2:  a1 + Minus(
     Sup({x30|Zero < x30 & x30 * x30 < a1})
      * Sup({x31|
     Zero < x31 & x31 * x31 < a1})) < 
     Three
      *