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

(* 69

BDED:

1:  Real(a1)
2:  Zero < a1


|-

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


*)


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



*)

NameSequent 19 "BDED"; 
(* 71 *)  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)"; 
(* 72 *)  r(); r(); l(); gl 2; l(); ThmCut "MPLUS"; 
(* 78 *)  l(); gl 7; gr 1; Done(); 
(* 82 *)  su 26 " Sup({x3|Zero < x3 & x3 * x3 < a1}) "; ThmCut "IPLUSb"; 
(* 84 *)  rwl 1; pl 1; ThmCut "SquareOrder1"; 
(* 87 *)  NextGoal(); 
(* 88 *)  NextGoal(); 
(* 89 *)  NextGoal(); 
(* 90 *)  NextGoal(); 
(* 91 *)  NextGoal(); 
(* 92 *)  NextGoal(); 
(* 93 *)  NextGoal(); 
(* 94 *)  NextGoal(); 
(* 95 *)  Done(); 
(* 96 *)  ThmCut "TRANS"; 
(* 97 *)  l(); r(); gl 8; gr 1; Done(); 
(* 102 *)  gl 3; gr 1; Done(); 
(* 105 *)  Done(); 
(* 106 *)  ThmCut "TRANS"; 
(* 107 *)  l(); r(); gl 8; gr 1; Done(); 
(* 112 *)  gl 3; gr 1; Done(); 
(* 115 *)  ThmCut "TRANS"; 
(* 116 *)  l(); r(); Done(); 
(* 119 *)  gl 2; gr 1; Done(); 
(* 122 *)  Done(); 
(* 123 *)  ThmCut "TRI"; 
(* 124 *)  su 39 "a1"; su 40 "[a23+Sup({x3|Zero < x3 & x3 * x3 < a1})]*[a23+Sup({x3|Zero < x3 & x3 * x3 < a1})]"; l(); NextGoal(); 
(* 128 *)  NextGoal(); 
(* 129 *)  NextGoal(); 
(* 130 *)  NextGoal(); 
(* 131 *)  NextGoal(); 
(* 132 *)  NextGoal(); 
(* 133 *)  NextGoal(); 
(* 134 *)  NextGoal(); 
(* 135 *)  l(); NextGoal(); 
(* 137 *)  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 *)  Cut "a23+Sup({x8|Zero < x8 & x8 * x8 < a1}) E {x3|Zero < x3 & x3 * x3 < a1}"; 
(* 153 *)  l(); l(); gl 8; w "a23+Sup({x3|Zero < x3 & x3 * x3 < a1})"; 
(* 157 *)  l(); r(); r(); gl 6; gr 1; Done(); 
(* 163 *)  gl 7; gr 1; Done(); 
(* 166 *)  pl 8; l(); l(); UseThm "NOTBOTH3" [10,1] []; 
(* 170 *)  UseThm "NOTBOTH" [1,10] []; 
(* 171 *)  r(); r(); ThmCut "TRANS"; 
(* 174 *)  l(); r(); gl 10; gr 1; Done(); 
(* 179 *)  gl 5; gr 1; Done(); 
(* 182 *)  ThmCut "TRANS"; 
(* 183 *)  l(); r(); Done(); 
(* 186 *)  gl 4; gr 1; Done(); 
(* 189 *)  Done(); 
(* 190 *)  Done(); 
(* 191 *)  NextGoal(); 
(* 192 *)  NextGoal(); 
(* 193 *)  NextGoal(); 
(* 194 *)  NextGoal(); 
(* 195 *)  NextGoal(); 
(* 196 *)  NextGoal(); 
(* 197 *)  NextGoal(); 
(* 198 *)  NextGoal(); 
(* 199 *)  ThmCut "EQUALITY"; 
(* 200 *)  NextGoal(); 
(* 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 *)  Done(); 
(* 217 *)  gl 8; gr 1; Done(); 
(* 220 *)  UseThm "RTIMES" [] [1]; 
(* 221 *)  ThmCut "FOIL"; 
(* 222 *)  rwl 1; pl 1; ThmCut "ORDERLEMMA1"; 
(* 225 *)  NextGoal(); 
(* 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 *)  gl 4; gr 1; gl 8; gr 1; Done(); 
(* 246 *)  gl 6; gr 1; Done(); 
(* 249 *)  gl 2; gl2 12; crwl 1; ThmCut "MPLUS"; 
(* 253 *)  l(); gl 9; gr 1; Done(); 
(* 257 *)  su 55 "Minus([Sup({x3|Zero < x3 & x3 * x3 < a1})]*[Sup({x3|Zero < x3 & x3 * x3 <a1})])"; ThmCut "MINUS"; 
(* 259 *)  rwl 1; pl 1; ThmCut "MPLUS"; 
(* 262 *)  l(); gl 3; gr 1; Done(); 
(* 266 *)  su 59 "Minus([Sup({x3|Zero < x3 & x3 * x3 < a1})]*[Sup({x3|Zero < x3 & x3 * x3 < a1})])"; ThmCut "APLUS"; 
(* 268 *)  rwl 1; pl 1; ThmCut "APLUS"; 
(* 271 *)  rwl ~1; pl 1; ThmCut "MINUS"; 
(* 274 *)  rwl 1; pl 1; ThmCut "IPLUSa"; 
(* 277 *)  rwl 1; pl 1; ThmCut "LIKETERMS1"; 
(* 280 *)  rwl 1; pl 1; ThmCut "CTIMES"; 
(* 283 *)  rwl 16; ThmCut "MTIMES"; 
(* 285 *)  l(); r(); Cut "Zero < Three*Sup({x3|Zero<x3 & x3*x3 <a1})"; 
(* 288 *)  UseThm "POSINV" [1] [1]; 
(* 289 *)  ThmCut "THREEPOS"; 
(* 290 *)  Cut "Zero <Sup({x3|Zero<x3 & x3*x3 <a1})"; 
(* 291 *)  UseThm "TIMESPOS" [2,1] [1]; 
(* 292 *)  pl 1; ThmCut "TRANS"; 
(* 294 *)  l(); r(); gl 15; gr 1; Done(); 
(* 299 *)  gl 10; gr 1; Done(); 
(* 302 *)  Done(); 
(* 303 *)  gl 2; gr 1; Done(); 
(* 306 *)  pl 6; pl 5; pl 2; ThmCut "ATIMES"; 
(* 310 *)  rwl 16; rwl 2; rwl 1; pl 1; ThmCut "ATIMES"; 
(* 315 *)  rwl 1; pl 1; ThmCut "CTIMES"; 
(* 318 *)  rwl 512; pl 1; ThmCut "ATIMES"; 
(* 321 *)  crwl 1; pl 1; ThmCut "ATIMES"; 
(* 324 *)  crwl 1; pl 1; ThmCut "INV"; 
(* 327 *)  l(); NextGoal(); 
(* 329 *)  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 *)  rwl 1; pl 1; ThmCut "ITIMES"; 
(* 395 *)  l(); NextGoal(); 
(* 397 *)  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 *)  UseThm "RTIMES" [] [1]; 
(* 509 *)  ThmCut "CTIMES"; 
(* 510 *)  rwl 1; gl 2; rwl 1; pl 1; pl 14; ThmCut "MTIMES"; 
(* 516 *)  l(); r(); Cut "Zero < Inv(Three*Sup({x3|Zero <x3 & x3*x3 < a1}))"; 
(* 519 *)  Done(); 
(* 520 *)  Cut "Zero < Three*Sup({x3|Zero<x3 & x3*x3 <a1})"; 
(* 521 *)  UseThm "POSINV" [1] [1]; 
(* 522 *)  ThmCut "THREEPOS"; 
(* 523 *)  Cut "Zero <Sup({x3|Zero<x3 & x3*x3 <a1})"; 
(* 524 *)  UseThm "TIMESPOS" [2,1] [1]; 
(* 525 *)  pl 1; ThmCut "TRANS"; 
(* 527 *)  l(); r(); gl 13; gr 1; Done(); 
(* 532 *)  gl 8; gr 1; Done(); 
(* 535 *)  Done(); 
(* 536 *)  gl 3; gr 1; Done(); 
(* 539 *)  ThmCut "MZERO2"; 
(* 540 *)  rwl 1; pl 1; r(); r(); gl 2; gr 2; Done(); 
(* 547 *)  gl 7; gr 1; Done(); 
(* 550 *)  ThmCut "EQUALITY"; 
(* 551 *)  NextGoal(); 
(* 552 *)  NextGoal(); 
(* 553 *)  NextGoal(); 
(* 554 *)  NextGoal(); 
(* 555 *)  UseThm "RSUP" [] [1]; 
(* 556 *)  NextGoal(); 
(* 557 *)  NextGoal(); 
(* 558 *)  NextGoal(); 
(* 559 *)  NextGoal(); 
(* 560 *)  UseThm "RTIMES" [] [1]; 
(* 561 *)  Done(); 
(* 562 *)  UseThm "RTIMES" [] [1]; 
(* 563 *)  UseThm "RZERO" [] [1]; 
(* 564 *)  gl2 4; rwl 1; ThmCut "ATIMES"; 
(* 567 *)  gl2 3; crwl 1; gl 16; gl2 3; rwl 1; ThmCut "MZERO2"; 
(* 573 *)  gl2 3; rwl 1; UseThm "NOTBOTH" [2,3] []; 
(* 576 *)  ThmCut "FOIL"; 
(* 577 *)  rwl 1; pl 1; ThmCut "ORDERLEMMA1"; 
(* 580 *)  NextGoal(); 
(* 581 *)  NextGoal(); 
(* 582 *)  NextGoal(); 
(* 583 *)  NextGoal(); 
(* 584 *)  gl 10; gr 1; Done(); 
(* 587 *)  gl 5; gr 1; Done(); 
(* 590 *)  ThmCut "TRANS"; 
(* 591 *)  l(); r(); gl 2; gr 1; Done(); 
(* 596 *)  Done(); 
(* 597 *)  pl 2; pl 2; ThmCut "MPLUS"; 
(* 600 *)  l(); gl 7; gr 1; Done(); 
(* 604 *)  su 117 "Minus([Sup({x3|Zero < x3 & x3 * x3 < a1})]*[Sup({x3|Zero < x3 & x3 * x3 <a1})])"; ThmCut "MINUS"; 
(* 606 *)  rwl 1; pl 1; ThmCut "MPLUS"; 
(* 609 *)  l(); gl 2; gr 1; Done(); 
(* 613 *)  su 121 "Minus([Sup({x3|Zero < x3 & x3 * x3 < a1})]*[Sup({x3|Zero < x3 & x3 * x3 < a1})])"; ThmCut "APLUS"; 
(* 615 *)  rwl ~1; pl 1; ThmCut "APLUS"; 
(* 618 *)  rwl ~1; pl 1; ThmCut "MINUS"; 
(* 621 *)  rwl 1; pl 1; ThmCut "IPLUSa"; 
(* 624 *)  rwl 1; pl 1; ThmCut "LIKETERMS1"; 
(* 627 *)  rwl 1; pl 1; ThmCut "CTIMES"; 
(* 630 *)  rwl 16; pl 1; ThmCut "MTIMES"; 
(* 633 *)  l(); r(); Cut "Zero < Three * Sup({x3|Zero <x3 & x3*x3 <a1})"; 
(* 636 *)  UseThm "POSINV" [1] [1]; 
(* 637 *)  ThmCut "THREEPOS"; 
(* 638 *)  Cut "Zero < Sup({x3|Zero<x3 & x3*x3 <a1})"; 
(* 639 *)  UseThm "TIMESPOS" [2,1] [1]; 
(* 640 *)  pl 1; ThmCut "TRANS"; 
(* 642 *)  l(); r(); gl 12; gr 1; Done(); 
(* 647 *)  gl 7; gr 1; Done(); 
(* 650 *)  Done(); 
(* 651 *)  Done(); 
(* 652 *)  ThmCut "ATIMES"; 
(* 653 *)  rwl 1; pl 1; ThmCut "ATIMES"; 
(* 656 *)  rwl 1; pl 1; ThmCut "CTIMES"; 
(* 659 *)  rwl 512; pl 1; ThmCut "ATIMES"; 
(* 662 *)  crwl 1; pl 1; ThmCut "ATIMES"; 
(* 665 *)  crwl 1; pl 1; ThmCut "INV"; 
(* 668 *)  l(); NextGoal(); 
(* 670 *)  NextGoal(); 
(* 671 *)  NextGoal(); 
(* 672 *)  NextGoal(); 
(* 673 *)  UseThm "RTIMES" [] [1]; 
(* 674 *)  UseThm "RTIMES" [] [1]; 
(* 675 *)  rwl 1; pl 1; ThmCut "ITIMES"; 
(* 678 *)  ThmCut "CTIMES"; 
(* 679 *)  rwl 1; gl 2; l(); gl 7; gr 1; Done(); 
(* 685 *)  rwl 1; pl 1; r(); r(); gl 1; gr 2; Done(); 
(* 692 *)  ThmCut "EQUALITY"; 
(* 693 *)  NextGoal(); 
(* 694 *)  NextGoal(); 
(* 695 *)  NextGoal(); 
(* 696 *)  NextGoal(); 
(* 697 *)  Done(); 
(* 698 *)  UseThm "RTIMES" [] [1]; 
(* 699 *)  UseThm "RZERO" [] [1]; 
(* 700 *)  pl 2; gl2 3; ThmCut "ATIMES"; 
(* 703 *)  gl2 3; crwl 1; pl 1; gl 14; rwl 1; pl 1; ThmCut "MZERO2"; 
(* 710 *)  rwl 1; pl 1; UseThm "NOTBOTH" [1,2] []; 
(* 713 *)