(* 1 *)  Start "(Ax1.Real(x1)&Zero<x1 ->(Ex2.x2*x2 = x1))"; 
(* 2 *)  r(); r(); l(); w "Sup({x3|Zero<x3 & x3*x3<a1})"; 
(* 6 *)  ThmCut "TRI"; 
(* 7 *)  l(); ThmCut "EQUALITY"; 
(* 9 *)  Done(); 
(* 10 *)  Done(); 
(* 11 *)  UseThm "RTIMES" [] [1]; 
(* 12 *)  gl 2; gr 1; Done(); 
(* 15 *)  l(); ThmCut "SUP2"; 
(* 17 *)  l(); r(); r(); su 6 "{x3|Zero < x3 & x3*x3 < a1}"; l(); l(); su 7 "a1 + One"; r(); r(); ThmCut "SqLemma"; 
(* 27 *)  ThmCut "TRANS"; 
(* 28 *)  l(); r(); gl 3; gr 1; Done(); 
(* 33 *)  Done(); 
(* 34 *)  ThmCut "SquareOrder2"; 
(* 35 *)  gl 1; gr 2; Done(); 
(* 38 *)  Done(); 
(* 39 *)  gl 3; gr 1; Done(); 
(* 42 *)  ThmCut "SQPOS"; 
(* 43 *)  su 14 "a8"; ThmCut "TRANS"; 
(* 45 *)  l(); r(); Done(); 
(* 48 *)  gl 5; gr 1; Done(); 
(* 51 *)  ThmCut "SOMETHINGBIGGER"; 
(* 52 *)  su 19 "a1"; ThmCut "TRANS"; 
(* 54 *)  l(); r(); gl 2; gr 1; Done(); 
(* 59 *)  Done(); 
(* 60 *)  Done(); 
(* 61 *)  gl 3; gr 1; Done(); 
(* 64 *)  gl 5; gr 1; Done(); 
(* 67 *)  gl 4; gr 1; Done(); 
(* 70 *)  Cut2 "(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)"; 
(* 71 *)  r(); r(); l(); gl 2; l(); ThmCut "MPLUS"; 
(* 77 *)  l(); gl 7; gr 1; Done(); 
(* 81 *)  su 26 " Sup({x3|Zero < x3 & x3 * x3 < a1}) "; ThmCut "IPLUSb"; 
(* 83 *)  rwl 1; pl 1; ThmCut "SquareOrder1"; 
(* 86 *)  NextGoal(); 
(* 87 *)  NextGoal(); 
(* 88 *)  NextGoal(); 
(* 89 *)  NextGoal(); 
(* 90 *)  NextGoal(); 
(* 91 *)  NextGoal(); 
(* 92 *)  NextGoal(); 
(* 93 *)  NextGoal(); 
(* 94 *)  Done(); 
(* 95 *)  ThmCut "TRANS"; 
(* 96 *)  l(); r(); gl 8; gr 1; Done(); 
(* 101 *)  gl 3; gr 1; Done(); 
(* 104 *)  Done(); ThmCut "TRANS"; 
(* 108 *)  l(); r(); gl 8; gr 1; Done(); 
(* 113 *)  gl 3; gr 1; Done(); 
(* 116 *)  ThmCut "TRANS"; 
(* 117 *)  l(); r(); Done(); 
(* 120 *)  gl 2; gr 1; Done(); 
(* 123 *)  Done(); 
(* 124 *)  ThmCut "TRI"; 
(* 125 *)  su 39 "a1"; su 40 "[a23+Sup({x3|Zero < x3 & x3 * x3 < a1})]*[a23+Sup({x3|Zero < x3 & x3 * x3 < a1})]"; l(); NextGoal(); 
(* 129 *)  NextGoal(); 
(* 130 *)  NextGoal(); 
(* 131 *)  NextGoal(); 
(* 132 *)  NextGoal(); 
(* 133 *)  NextGoal(); 
(* 134 *)  NextGoal(); 
(* 135 *)  NextGoal(); 
(* 136 *)  l(); NextGoal(); 
(* 138 *)  NextGoal(); 
(* 139 *)  NextGoal(); 
(* 140 *)  NextGoal(); 
(* 141 *)  NextGoal(); 
(* 142 *)  NextGoal(); 
(* 143 *)  NextGoal(); 
(* 144 *)  NextGoal(); 
(* 145 *)  NextGoal(); 
(* 146 *)  NextGoal(); 
(* 147 *)  NextGoal(); 
(* 148 *)  NextGoal(); 
(* 149 *)  NextGoal(); 
(* 150 *)  NextGoal(); 
(* 151 *)  NextGoal(); 
(* 152 *)  NextGoal(); 
(* 153 *)  Cut "a23+Sup({x8|Zero < x8 & x8 * x8 < a1}) E {x3|Zero < x3 & x3 * x3 < a1}"; 
(* 154 *)  l(); l(); gl 8; w "a23+Sup({x3|Zero < x3 & x3 * x3 < a1})"; 
(* 158 *)  l(); r(); r(); gl 6; gr 1; Done(); 
(* 164 *)  gl 7; gr 1; Done(); 
(* 167 *)  pl 8; l(); l(); UseThm "NOTBOTH3" [10,1] []; 
(* 171 *)  UseThm "NOTBOTH" [1,10] []; 
(* 172 *)  r(); r(); ThmCut "TRANS"; 
(* 175 *)  l(); r(); gl 10; gr 1; Done(); 
(* 180 *)  gl 5; gr 1; Done(); 
(* 183 *)  ThmCut "TRANS"; 
(* 184 *)  l(); r(); Done(); 
(* 187 *)  gl 4; gr 1; Done(); 
(* 190 *)  Done(); 
(* 191 *)  Done(); 
(* 192 *)  NextGoal(); 
(* 193 *)  NextGoal(); 
(* 194 *)  NextGoal(); 
(* 195 *)  NextGoal(); 
(* 196 *)  NextGoal(); 
(* 197 *)  NextGoal(); 
(* 198 *)  NextGoal(); 
(* 199 *)  NextGoal(); 
(* 200 *)  ThmCut "EQUALITY"; 
(* 201 *)  NextGoal(); 
(* 202 *)  NextGoal(); 
(* 203 *)  NextGoal(); 
(* 204 *)  NextGoal(); 
(* 205 *)  NextGoal(); 
(* 206 *)  NextGoal(); 
(* 207 *)  NextGoal(); 
(* 208 *)  NextGoal(); 
(* 209 *)  NextGoal(); 
(* 210 *)  NextGoal(); 
(* 211 *)  NextGoal(); 
(* 212 *)  NextGoal(); 
(* 213 *)  NextGoal(); 
(* 214 *)  NextGoal(); 
(* 215 *)  NextGoal(); 
(* 216 *)  NextGoal(); 
(* 217 *)  Done(); 
(* 218 *)  gl 8; gr 1; Done(); 
(* 221 *)  UseThm "RTIMES" [] [1]; 
(* 222 *)  ThmCut "FOIL"; 
(* 223 *)  rwl 1; pl 1; ThmCut "ORDERLEMMA1"; 
(* 226 *)  NextGoal(); 
(* 227 *)  NextGoal(); 
(* 228 *)  NextGoal(); 
(* 229 *)  NextGoal(); 
(* 230 *)  NextGoal(); 
(* 231 *)  NextGoal(); 
(* 232 *)  NextGoal(); 
(* 233 *)  NextGoal(); 
(* 234 *)  NextGoal(); 
(* 235 *)  NextGoal(); 
(* 236 *)  NextGoal(); 
(* 237 *)  NextGoal(); 
(* 238 *)  NextGoal(); 
(* 239 *)  NextGoal(); 
(* 240 *)  NextGoal(); 
(* 241 *)  NextGoal(); 
(* 242 *)  gl 4; gr 1; gl 8; gr 1; Done(); 
(* 247 *)  gl 6; gr 1; Done(); 
(* 250 *)  gl 2; gl2 12; crwl 1; ThmCut "MPLUS"; 
(* 254 *)  l(); gl 9; gr 1; Done(); 
(* 258 *)  su 55 "Minus([Sup({x3|Zero < x3 & x3 * x3 < a1})]*[Sup({x3|Zero < x3 & x3 * x3 <a1})])"; ThmCut "MINUS"; 
(* 260 *)  rwl 1; pl 1; ThmCut "MPLUS"; 
(* 263 *)  l(); gl 3; gr 1; Done(); 
(* 267 *)  su 59 "Minus([Sup({x3|Zero < x3 & x3 * x3 < a1})]*[Sup({x3|Zero < x3 & x3 * x3 < a1})])"; ThmCut "APLUS"; 
(* 269 *)  rwl 1; pl 1; ThmCut "APLUS"; 



(* 272 *)  rwl ~1; pl 1; ThmCut "MINUS"; 



(* 275 *)  rwl 1; pl 1; ThmCut "IPLUSa"; 



(* 278 *)  rwl 1; pl 1; ThmCut "LIKETERMS1"; 
(* 281 *)  rwl 1; pl 1; ThmCut "CTIMES"; 
(* 284 *)  rwl 16; ThmCut "MTIMES"; 
(* 286 *)  l(); r(); Cut "Zero < Three*Sup({x3|Zero<x3 & x3*x3 <a1})"; 
(* 289 *)  UseThm "POSINV" [1] [1]; 
(* 290 *)  ThmCut "THREEPOS"; 
(* 291 *)  Cut "Zero <Sup({x3|Zero<x3 & x3*x3 <a1})"; 
(* 292 *)  UseThm "TIMESPOS" [2,1] [1]; 
(* 293 *)  pl 1; ThmCut "TRANS"; 
(* 295 *)  l(); r(); gl 15; gr 1; Done(); 
(* 300 *)  gl 10; gr 1; Done(); 
(* 303 *)  Done(); 
(* 304 *)  gl 2; gr 1; Done(); 
(* 307 *)  pl 6; pl 5; pl 2; ThmCut "ATIMES"; 
(* 311 *)  rwl 16; rwl 2; rwl 1; pl 1; ThmCut "ATIMES"; 
(* 316 *)  rwl 1; pl 1; ThmCut "CTIMES"; 
(* 319 *)  rwl 512; pl 1; ThmCut "ATIMES"; 
(* 322 *)  crwl 1; pl 1; ThmCut "ATIMES"; 
(* 325 *)  crwl 1; pl 1; ThmCut "INV"; 
(* 328 *)  l(); NextGoal(); 
(* 330 *)  NextGoal(); 
(* 331 *)  NextGoal(); 
(* 332 *)  NextGoal(); 
(* 333 *)  NextGoal(); 
(* 334 *)  NextGoal(); 
(* 335 *)  NextGoal(); 
(* 336 *)  NextGoal(); 
(* 337 *)  NextGoal(); 
(* 338 *)  NextGoal(); 
(* 339 *)  NextGoal(); 
(* 340 *)  NextGoal(); 
(* 341 *)  NextGoal(); 
(* 342 *)  NextGoal(); 
(* 343 *)  NextGoal(); 
(* 344 *)  NextGoal(); 
(* 345 *)  NextGoal(); 
(* 346 *)  NextGoal(); 
(* 347 *)  NextGoal(); 
(* 348 *)  NextGoal(); 
(* 349 *)  NextGoal(); 
(* 350 *)  NextGoal(); 
(* 351 *)  NextGoal(); 
(* 352 *)  NextGoal(); 
(* 353 *)  NextGoal(); 
(* 354 *)  NextGoal(); 
(* 355 *)  NextGoal(); 
(* 356 *)  NextGoal(); 
(* 357 *)  NextGoal(); 
(* 358 *)  NextGoal(); 
(* 359 *)  NextGoal(); 
(* 360 *)  NextGoal(); 
(* 361 *)  NextGoal(); 
(* 362 *)  NextGoal(); 
(* 363 *)  NextGoal(); 
(* 364 *)  NextGoal(); 
(* 365 *)  NextGoal(); 
(* 366 *)  NextGoal(); 
(* 367 *)  NextGoal(); 
(* 368 *)  NextGoal(); 
(* 369 *)  NextGoal(); 
(* 370 *)  NextGoal(); 
(* 371 *)  NextGoal(); 
(* 372 *)  NextGoal(); 
(* 373 *)  NextGoal(); 
(* 374 *)  NextGoal(); 
(* 375 *)  NextGoal(); 
(* 376 *)  NextGoal(); 
(* 377 *)  NextGoal(); 
(* 378 *)  NextGoal(); 
(* 379 *)  NextGoal(); 
(* 380 *)  NextGoal(); 
(* 381 *)  NextGoal(); 
(* 382 *)  NextGoal(); 
(* 383 *)  NextGoal(); 
(* 384 *)  NextGoal(); 
(* 385 *)  NextGoal(); 
(* 386 *)  NextGoal(); 
(* 387 *)  NextGoal(); 
(* 388 *)  NextGoal(); 
(* 389 *)  NextGoal(); 
(* 390 *)  NextGoal(); 
(* 391 *)  NextGoal(); 
(* 392 *)  NextGoal(); 
(* 393 *)  rwl 1; pl 1; ThmCut "ITIMES"; 
(* 396 *)  l(); NextGoal(); 
(* 398 *)  NextGoal(); 
(* 399 *)  NextGoal(); 
(* 400 *)  NextGoal(); 
(* 401 *)  NextGoal(); 
(* 402 *)  NextGoal(); 
(* 403 *)  NextGoal(); 
(* 404 *)  NextGoal(); 
(* 405 *)  NextGoal(); 
(* 406 *)  NextGoal(); 
(* 407 *)  NextGoal(); 
(* 408 *)  NextGoal(); 
(* 409 *)  NextGoal(); 
(* 410 *)  NextGoal(); 
(* 411 *)  NextGoal(); 
(* 412 *)  NextGoal(); 
(* 413 *)  NextGoal(); 
(* 414 *)  NextGoal(); 
(* 415 *)  NextGoal(); 
(* 416 *)  NextGoal(); 
(* 417 *)  NextGoal(); 
(* 418 *)  NextGoal(); 
(* 419 *)  NextGoal(); 
(* 420 *)  NextGoal(); 
(* 421 *)  NextGoal(); 
(* 422 *)  NextGoal(); 
(* 423 *)  NextGoal(); 
(* 424 *)  NextGoal(); 
(* 425 *)  NextGoal(); 
(* 426 *)  NextGoal(); 
(* 427 *)  NextGoal(); 
(* 428 *)  NextGoal(); 
(* 429 *)  NextGoal(); 
(* 430 *)  NextGoal(); 
(* 431 *)  NextGoal(); 
(* 432 *)  NextGoal(); 
(* 433 *)  NextGoal(); 
(* 434 *)  NextGoal(); 
(* 435 *)  NextGoal(); 
(* 436 *)  NextGoal(); 
(* 437 *)  NextGoal(); 
(* 438 *)  NextGoal(); 
(* 439 *)  NextGoal(); 
(* 440 *)  NextGoal(); 
(* 441 *)  NextGoal(); 
(* 442 *)  NextGoal(); 
(* 443 *)  NextGoal(); 
(* 444 *)  NextGoal(); 
(* 445 *)  NextGoal(); 
(* 446 *)  NextGoal(); 
(* 447 *)  NextGoal(); 
(* 448 *)  NextGoal(); 
(* 449 *)  NextGoal(); 
(* 450 *)  NextGoal(); 
(* 451 *)  NextGoal(); 
(* 452 *)  NextGoal(); 
(* 453 *)  NextGoal(); 
(* 454 *)  NextGoal(); 
(* 455 *)  NextGoal(); 
(* 456 *)  NextGoal(); 
(* 457 *)  NextGoal(); 
(* 458 *)  NextGoal(); 
(* 459 *)  NextGoal(); 
(* 460 *)  NextGoal(); 
(* 461 *)  NextGoal(); 
(* 462 *)  NextGoal(); 
(* 463 *)  NextGoal(); 
(* 464 *)  NextGoal(); 
(* 465 *)  NextGoal(); 
(* 466 *)  NextGoal(); 
(* 467 *)  NextGoal(); 
(* 468 *)  NextGoal(); 
(* 469 *)  NextGoal(); 
(* 470 *)  NextGoal(); 
(* 471 *)  NextGoal(); 
(* 472 *)  NextGoal(); 
(* 473 *)  NextGoal(); 
(* 474 *)  NextGoal(); 
(* 475 *)  NextGoal(); 
(* 476 *)  NextGoal(); 
(* 477 *)  NextGoal(); 
(* 478 *)  NextGoal(); 
(* 479 *)  NextGoal(); 
(* 480 *)  NextGoal(); 
(* 481 *)  NextGoal(); 
(* 482 *)  NextGoal(); 
(* 483 *)  NextGoal(); 
(* 484 *)  NextGoal(); 
(* 485 *)  NextGoal(); 
(* 486 *)  NextGoal(); 
(* 487 *)  NextGoal(); 
(* 488 *)  NextGoal(); 
(* 489 *)  NextGoal(); 
(* 490 *)  NextGoal(); 
(* 491 *)  NextGoal(); 
(* 492 *)  NextGoal(); 
(* 493 *)  NextGoal(); 
(* 494 *)  NextGoal(); 
(* 495 *)  NextGoal(); 
(* 496 *)  NextGoal(); 
(* 497 *)  NextGoal(); 
(* 498 *)  NextGoal(); 
(* 499 *)  NextGoal(); 
(* 500 *)  NextGoal(); 
(* 501 *)  NextGoal(); 
(* 502 *)  NextGoal(); 
(* 503 *)  NextGoal(); 
(* 504 *)  NextGoal(); 
(* 505 *)  NextGoal(); 
(* 506 *)  NextGoal(); 
(* 507 *)  NextGoal(); 
(* 508 *)  NextGoal(); 
(* 509 *)  UseThm "RTIMES" [] [1]; 
(* 510 *)  ThmCut "CTIMES"; 
(* 511 *)  rwl 1; gl 2; rwl 1; pl 1; pl 14; ThmCut "MTIMES"; 
(* 517 *)  l(); r(); Cut "Zero < Inv(Three*Sup({x3|Zero <x3 & x3*x3 < a1}))"; 
(* 520 *)  Done(); 
(* 521 *)  Cut "Zero < Three*Sup({x3|Zero<x3 & x3*x3 <a1})"; 
(* 522 *)  UseThm "POSINV" [1] [1]; 
(* 523 *)  ThmCut "THREEPOS"; 
(* 524 *)  Cut "Zero <Sup({x3|Zero<x3 & x3*x3 <a1})"; 
(* 525 *)  UseThm "TIMESPOS" [2,1] [1]; 
(* 526 *)  pl 1; ThmCut "TRANS"; 
(* 528 *)  l(); r(); gl 13; gr 1; Done(); 
(* 533 *)  gl 8; gr 1; Done(); 
(* 536 *)  Done(); 
(* 537 *)  gl 3; gr 1; Done(); 
(* 540 *)  ThmCut "MZERO2"; 
(* 541 *)  rwl 1; pl 1; r(); r(); gl 2; gr 2; Done(); 
(* 548 *)  gl 7; gr 1; Done(); 
(* 551 *)  ThmCut "EQUALITY"; 
(* 552 *)  NextGoal(); 
(* 553 *)  NextGoal(); 
(* 554 *)  NextGoal(); 
(* 555 *)  NextGoal(); 
(* 556 *)  UseThm "RSUP" [] [1]; 
(* 557 *)  NextGoal(); 
(* 558 *)  NextGoal(); 
(* 559 *)  NextGoal(); 
(* 560 *)  NextGoal(); 
(* 561 *)  UseThm "RTIMES" [] [1]; 
(* 562 *)  Done(); 
(* 563 *)  UseThm "RTIMES" [] [1]; 
(* 564 *)  UseThm "RZERO" [] [1]; 
(* 565 *)  gl2 4; rwl 1; ThmCut "ATIMES"; 
(* 568 *)  gl2 3; crwl 1; gl 16; gl2 3; rwl 1; ThmCut "MZERO2"; 
(* 574 *)  gl2 3; rwl 1; UseThm "NOTBOTH" [2,3] []; 
(* 577 *)  

(* 576

Now case two, x < (y+e)(y+e)*)


(* Sequent snapshot:
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)



*)

ThmCut "FOIL"; 
(* 578 *)  rwl 1; pl 1; ThmCut "ORDERLEMMA1"; 
(* 581 *)  NextGoal(); 
(* 582 *)  NextGoal(); 
(* 583 *)  NextGoal(); 
(* 584 *)  NextGoal(); 
(* 585 *)  gl 10; gr 1; Done(); 
(* 588 *)  gl 5; gr 1; Done(); 
(* 591 *)  ThmCut "TRANS"; 
(* 592 *)  l(); r(); gl 2; gr 1; Done(); 
(* 597 *)  Done(); 
(* 598 *)  pl 2; pl 2; ThmCut "MPLUS"; 
(* 601 *)  l(); gl 7; gr 1; Done(); 
(* 605 *)  su 117 "Minus([Sup({x3|Zero < x3 & x3 * x3 < a1})]*[Sup({x3|Zero < x3 & x3 * x3 <a1})])"; ThmCut "MINUS"; 
(* 607 *)  rwl 1; pl 1; ThmCut "MPLUS"; 
(* 610 *)  l(); gl 2; gr 1; Done(); 
(* 614 *)  su 121 "Minus([Sup({x3|Zero < x3 & x3 * x3 < a1})]*[Sup({x3|Zero < x3 & x3 * x3 < a1})])"; ThmCut "APLUS"; 
(* 616 *)  rwl ~1; pl 1; ThmCut "APLUS"; 
(* 619 *)  rwl ~1; pl 1; ThmCut "MINUS"; 
(* 622 *)  rwl 1; pl 1; ThmCut "IPLUSa"; 
(* 625 *)  rwl 1; pl 1; ThmCut "LIKETERMS1"; 
(* 628 *)  rwl 1; pl 1; ThmCut "CTIMES"; 
(* 631 *)  rwl 16; pl 1; ThmCut "MTIMES"; 
(* 634 *)  l(); r(); Cut "Zero < Three * Sup({x3|Zero <x3 & x3*x3 <a1})"; 
(* 637 *)  UseThm "POSINV" [1] [1]; 
(* 638 *)  ThmCut "THREEPOS"; 
(* 639 *)  Cut "Zero < Sup({x3|Zero<x3 & x3*x3 <a1})"; 
(* 640 *)  UseThm "TIMESPOS" [2,1] [1]; 
(* 641 *)  pl 1; ThmCut "TRANS"; 
(* 643 *)  l(); r(); gl 12; gr 1; Done(); 
(* 648 *)  gl 7; gr 1; Done(); 
(* 651 *)  Done(); 
(* 652 *)  Done(); 
(* 653 *)  ThmCut "ATIMES"; 
(* 654 *)  rwl 1; pl 1; ThmCut "ATIMES"; 
(* 657 *)  rwl 1; pl 1; ThmCut "CTIMES"; 
(* 660 *)  rwl 512; pl 1; ThmCut "ATIMES"; 
(* 663 *)  crwl 1; pl 1; ThmCut "ATIMES"; 
(* 666 *)  crwl 1; pl 1; ThmCut "INV"; 
(* 669 *)  l(); NextGoal(); 
(* 671 *)  NextGoal(); 
(* 672 *)  NextGoal(); 
(* 673 *)  NextGoal();
(* 674 *)  UseThm "RTIMES" [] [1]; 
(* 675 *)  UseThm "RTIMES" [] [1]; 
(* 676 *)  rwl 1; pl 1; ThmCut "ITIMES"; 
(* 679 *)  ThmCut "CTIMES"; 
(* 680 *)  rwl 1; gl 2; l(); gl 7; gr 1;  Done(); 
(* 734 *)  rwl 1; pl 1; r(); r(); gl 1; gr 2; Done(); 
(* 741 *)  ThmCut "EQUALITY"; 
(* 742 *)  NextGoal(); 
(* 743 *)  NextGoal(); 
(* 744 *)  NextGoal(); 
(* 745 *)  NextGoal(); 
(* 746 *)  Done(); 
(* 747 *)  UseThm "RTIMES" [] [1]; 
(* 748 *)  UseThm "RZERO" [] [1]; 
(* 749 *)  pl 2; gl2 3; ThmCut "ATIMES"; 
(* 752 *)  gl2 3; crwl 1; pl 1; gl 14; rwl 1; pl 1; ThmCut "MZERO2"; 
(* 759 *)  rwl 1; pl 1; UseThm "NOTBOTH" [1,2] []; 

(* THROUGH TO EPSILON!!
(* 762 *)  

(* 761

some mess above, now for eps*)


(* 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)



*)

w "a23"; 
(* 763 *)  l(); r(); ThmCut "EPSLEMMA1"; 
(* 766 *)  NextGoal(); 
(* 767 *)  NextGoal(); 
(* 768 *)  NextGoal(); 
(* 769 *)  NextGoal(); 
(* 770 *)  NextGoal(); 
(* 771 *)  NextGoal(); 
(* 772 *)  NextGoal(); 
(* 773 *)  NextGoal(); 
(* 774 *)  Cut "Zero <= [a1 + Minus(Sup({x13|Zero < x13 & x13 * x13 < a1})* Sup({x14|Zero < x14 & x14 * x14 < a1}))] * Inv(Three* Sup({x15|Zero < x15 & x15 * x15 < a1}))"; 
(* 775 *)  Done(); 
(* 776 *)  Undo(); Undo(); NextGoal(); 
(* 779 *)  NextGoal(); 
(* 780 *)  NextGoal(); 
(* 781 *)  NextGoal(); 
(* 782 *)  w "a23"; 
(* 783 *)  l(); Undo(); 

(* 784

where AM i?*)


(* Sequent snapshot:
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:  (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)
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


|-

1:  Real(a23)
      & a23 < Sup({x4|Zero < x4 & x4 * x4 < a1})
2:  
     Sup({x3|Zero < x3 & x3 * x3 < a1}) * Sup({x3|Zero < x3 & x3
      * x3 < a1}) = a1
3:  (Ex3.x3 * x3 = a1)



*)*)