:: Arithmetic of Non Negative Rational Numbers
::  by Grzegorz Bancerek
::
:: Received March 7, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ORDINAL1, XBOOLE_0, ORDINAL2, TARSKI, SUBSET_1, ORDINAL3,
      ARYTM_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, ORDINAL3;
 constructors SUBSET_1, ORDINAL3;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, ORDINAL3;
 requirements BOOLE, SUBSET, NUMERALS;
 definitions TARSKI, ORDINAL1;
 theorems TARSKI, XBOOLE_0, ZFMISC_1, ORDINAL1, ORDINAL2, ORDINAL3, XBOOLE_1,
      XTUPLE_0;
 schemes ORDINAL1;

begin :: Natural ordinals

reserve A,B,C for Ordinal;

Lm1: {} in omega by ORDINAL1:def 11;

Lm2: 1 in omega;

definition
  func one equals
  1;
  correctness;
end;

begin :: Relative prime numbers and divisibility

definition
  let a,b be Ordinal;
  pred a,b are_relative_prime means
  :Def2:
  for c,d1,d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds c = 1;
  symmetry;
end;

theorem
  not {},{} are_relative_prime
proof
  take {}, {}, {};
  thus thesis by ORDINAL2:35;
end;

theorem Th2:
  1,A are_relative_prime
proof
  let c,d1,d2 be Ordinal;
  thus thesis by ORDINAL3:37;
end;

theorem Th3:
  {},A are_relative_prime implies A = 1
proof
A1: {} = A*^{} & A = A*^1 by ORDINAL2:38,39;
  assume {},A are_relative_prime & A <> 1;
  hence contradiction by A1,Def2;
end;

reserve a,b,c,d for natural Ordinal;

defpred PP[set] means ex B st B c= $1 & $1 in omega & $1 <> {} & not ex c,d1,
d2 being natural Ordinal st d1,d2 are_relative_prime & $1 = c *^ d1 & B = c *^
d2;

theorem
  a <> {} or b <> {} implies ex c,d1,d2 being natural Ordinal st d1,d2
  are_relative_prime & a = c *^ d1 & b = c *^ d2
proof
  assume that
A1: a <> {} or b <> {} and
A2: not ex c,d1,d2 being natural Ordinal st d1,d2 are_relative_prime & a
  = c *^ d1 & b = c *^ d2;
A3: ex A st PP[A]
  proof
    per cases;
    suppose
A4:   a c= b;
      take A = b, B = a;
      thus B c= A & A in omega & A <> {} by A1,A4,ORDINAL1:def 12;
      thus thesis by A2;
    end;
    suppose
A5:   b c= a;
      take A = a, B = b;
      thus B c= A & A in omega & A <> {} by A1,A5,ORDINAL1:def 12;
      thus thesis by A2;
    end;
  end;
  consider A such that
A6: PP[A] and
A7: for C st PP[C] holds A c= C from ORDINAL1:sch 1(A3);
  consider B such that
A8: B c= A and
A9: A in omega and
A10: A <> {} and
A11: not ex c,d1,d2 being natural Ordinal st d1,d2 are_relative_prime &
  A = c *^ d1 & B = c *^ d2 by A6;
  reconsider A,B as Element of omega by A8,A9,ORDINAL1:12;
  A = 1 *^ A & B = 1 *^ B by ORDINAL2:39;
  then not A,B are_relative_prime by A11;
  then consider c,d1,d2 being Ordinal such that
A12: A = c *^ d1 and
A13: B = c *^ d2 and
A14: c <> 1 by Def2;
A15: c <> {} by A10,A12,ORDINAL2:35;
  then
A16: d1 c= A & d2 c= B by A12,A13,ORDINAL3:36;
A17: d1 <> {} by A10,A12,ORDINAL2:38;
  then c c= A by A12,ORDINAL3:36;
  then reconsider c,d1,d2 as Element of omega by A16,ORDINAL1:12;
  1 in c or c in 1 by A14,ORDINAL1:14;
  then 1*^d1 in A by A12,A17,A15,ORDINAL3:14,19;
  then
A18: d1 in A by ORDINAL2:39;
A19: now
    let c9,d19,d29 be natural Ordinal;
    assume that
A20: d19,d29 are_relative_prime and
A21: d1 = c9 *^ d19 & d2 = c9 *^ d29;
    A = c*^c9*^d19 & B = c*^c9*^d29 by A12,A13,A21,ORDINAL3:50;
    hence contradiction by A11,A20;
  end;
  A = d1*^c & B = d2*^c by A12,A13;
  then d2 c= d1 by A8,A15,ORDINAL3:35;
  hence contradiction by A7,A17,A19,A18,ORDINAL1:5;
end;

reserve l,m,n for natural Ordinal;

registration
  let m,n;
  cluster m div^ n -> natural;
  coherence
  proof
A1: n = {} implies m div^ n = {} & {}*^1 = {} by ORDINAL2:35,ORDINAL3:def 6;
    n in 1 or 1 c= n by ORDINAL1:16;
    then (m div^ n)*^1 c= (m div^ n)*^n by A1,ORDINAL3:14,20;
    then
A2: m div^ n c= (m div^ n)*^n by ORDINAL2:39;
    (m div^ n)*^n c= m & m in omega by ORDINAL1:def 12,ORDINAL3:64;
    hence m div^ n in omega by A2,ORDINAL1:12,XBOOLE_1:1;
  end;
  cluster m mod^ n -> natural;
  coherence
  proof
    (m div^ n)*^n+^(m mod^ n) = m by ORDINAL3:65;
    then
A3: m mod^ n c= m by ORDINAL3:24;
    m in omega by ORDINAL1:def 12;
    hence m mod^ n in omega by A3,ORDINAL1:12;
  end;
end;

definition
  let k,n be Ordinal;
  pred k divides n means
  : Def3:
  ex a being Ordinal st n = k*^a;
  reflexivity
  proof
    let n be Ordinal;
    take 1;
    thus thesis by ORDINAL2:39;
  end;
end;

theorem Th5:
  a divides b iff ex c st b = a*^c
proof
  thus a divides b implies ex c st b = a*^c
  proof
    given c being Ordinal such that
A1: b = a*^c;
    per cases;
    suppose
      b = {};
      then b = a*^{} by ORDINAL2:38;
      hence thesis;
    end;
    suppose
      b <> {};
      then c is Element of omega by A1,ORDINAL3:75;
      hence thesis by A1;
    end;
  end;
  thus thesis by Def3;
end;

theorem Th6:
  for m,n st {} in m holds n mod^ m in m
proof
  let m,n;
  assume {} in m;
  then
A1: ex C st n = (n div^ m)*^m+^C & C in m by ORDINAL3:def 6;
  n mod^ m = n-^(n div^ m)*^m by ORDINAL3:def 7;
  hence thesis by A1,ORDINAL3:52;
end;

theorem Th7:
  for n,m holds m divides n iff n = m *^ (n div^ m)
proof
  let n,m;
  assume
A1: not thesis;
  then consider a such that
A2: n = m*^a by Th5;
  {}*^a = {} by ORDINAL2:35;
  then {} <> m by A1,A2,ORDINAL2:35;
  then
A3: {} in m by ORDINAL3:8;
  n = a*^m+^{} by A2,ORDINAL2:27;
  hence thesis by A1,A2,A3,Def3,ORDINAL3:def 6;
end;

theorem Th8:
  for n,m st n divides m & m divides n holds n = m
proof
  let n,m;
  assume that
A1: n divides m and
A2: m divides n;
A3: m = n *^ (m div^ n) by A1,Th7;
A4: (m div^ n) *^ (n div^ m) = 1 implies n = m
  proof
    assume (m div^ n) *^ (n div^ m) = 1;
    then m div^ n = 1 by ORDINAL3:37;
    hence thesis by A3,ORDINAL2:39;
  end;
  n = m *^ (n div^ m) by A2,Th7;
  then
A5: n *^ 1 = n & n = n *^ ((m div^ n) *^ (n div^ m)) by A3,ORDINAL2:39
,ORDINAL3:50;
  n = {} implies n = m by A3,ORDINAL2:35;
  hence thesis by A5,A4,ORDINAL3:33;
end;

theorem Th9:
  n divides {} & 1 divides n
proof
  {} = n *^ {} by ORDINAL2:35;
  hence n divides {} by Def3;
  n = 1 *^ n by ORDINAL2:39;
  hence thesis by Def3;
end;

theorem Th10:
  for n,m st {} in m & n divides m holds n c= m
proof
  let n,m such that
A1: {} in m;
  given a being Ordinal such that
A2: m = n*^a;
  a <> {} by A1,A2,ORDINAL2:38;
  hence thesis by A2,ORDINAL3:36;
end;

theorem Th11:
  for n,m,l st n divides m & n divides m +^ l holds n divides l
proof
  let n,m,l;
  assume n divides m;
  then consider a such that
A1: m = n*^a by Th5;
  assume n divides m +^ l;
  then consider b such that
A2: m +^ l = n*^b by Th5;
  assume
A3: not n divides l;
  l = n*^b -^ n*^a by A1,A2,ORDINAL3:52
    .= (b-^a)*^n by ORDINAL3:63;
  hence thesis by A3,Def3;
end;

Lm3: 1 = succ {};

definition
  let k,n be natural Ordinal;
  func k lcm n -> Element of omega means
  : Def4:
  k divides it & n divides it &
  for m st k divides m & n divides m holds it divides m;
  existence
  proof
    per cases;
    suppose
A1:   k = {} or n = {};
      reconsider w = {} as Element of omega by ORDINAL1:def 12;
      take w;
      thus k divides w & n divides w by Th9;
      let m;
      assume k divides m & n divides m;
      hence thesis by A1;
    end;
    suppose
A2:   k <> {} & n <> {};
      {} c= k;
      then {} c< k by A2,XBOOLE_0:def 8;
      then
A3:   {} in k by ORDINAL1:11;
      {} c= n;
      then {} c< n by A2,XBOOLE_0:def 8;
      then {} in n by ORDINAL1:11;
      then
A4:   1 c= n by Lm3,ORDINAL1:21;
      defpred P[Ordinal] means ex m st $1 = m & k divides m & n divides m & k
      c= m;
A5:   k*^1 = k by ORDINAL2:39;
      k divides k *^ n & n divides k *^ n by Def3;
      then
A6:   ex A st P[A] by A4,A5,ORDINAL2:41;
      consider A such that
A7:   P[A] and
A8:   for B st P[B] holds A c= B from ORDINAL1:sch 1(A6);
      consider l such that
A9:   A = l and
A10:  k divides l and
A11:  n divides l and
A12:  k c= l by A7;
      reconsider l as Element of omega by ORDINAL1:def 12;
      take l;
      thus k divides l & n divides l by A10,A11;
      let m such that
A13:  k divides m and
A14:  n divides m;
A15:  m = l*^(m div^ l)+^(m mod^ l) by ORDINAL3:65;
      l = k*^(l div^ k) by A10,Th7;
      then l*^(m div^ l) = k*^((l div^ k)*^(m div^ l)) by ORDINAL3:50;
      then k divides l*^(m div^ l) by Def3;
      then
A16:  k divides m mod^ l by A13,A15,Th11;
      l = n*^(l div^ n) by A11,Th7;
      then l*^(m div^ l) = n*^((l div^ n)*^(m div^ l)) by ORDINAL3:50;
      then n divides l*^(m div^ l) by Def3;
      then
A17:  n divides m mod^ l by A14,A15,Th11;
      now
A18:    {} c= m mod^ l;
        assume m mod^ l <> {};
        then {} c< m mod^ l by A18,XBOOLE_0:def 8;
        then k c= m mod^ l by A16,Th10,ORDINAL1:11;
        then l c= m mod^ l by A8,A9,A16,A17;
        hence contradiction by A12,A3,Th6,ORDINAL1:5;
      end;
      then m = l*^(m div^ l) by A15,ORDINAL2:27;
      hence thesis by Th7;
    end;
  end;
  uniqueness
  proof
    let m1,m2 be Element of omega;
    assume k divides m1 & n divides m1 & ( for m st k divides m & n divides
m holds m1 divides m)& k divides m2 &( n divides m2 & for m st k divides m & n
    divides m holds m2 divides m );
    then m1 divides m2 & m2 divides m1;
    hence thesis by Th8;
  end;
  commutativity;
end;

theorem Th12:
  m lcm n divides m*^n
proof
  m divides m*^n & n divides m*^n by Def3;
  hence thesis by Def4;
end;

theorem Th13:
  n <> {} implies (m*^n) div^ (m lcm n) divides m
proof
  assume
A1: n <> {};
  take ((m lcm n) div^ n);
  n divides m lcm n by Def4;
  then
A2: m lcm n = n*^((m lcm n) div^ n) by Th7;
  m lcm n divides m*^n by Th12;
  then m*^n = (m lcm n)*^ ((m*^n) div^ (m lcm n)) by Th7;
  then n*^m = n*^(((m lcm n) div^ n)*^ ((m*^n) div^ (m lcm n))) by A2,
ORDINAL3:50;
  hence m = ((m*^n) div^ (m lcm n))*^((m lcm n) div^ n) by A1,ORDINAL3:33;
end;

definition
  let k,n be natural Ordinal;
  func k hcf n -> Element of omega means
  : Def5:
  it divides k & it divides n &
  for m st m divides k & m divides n holds m divides it;
  existence
  proof
    per cases;
    suppose
A1:   k = {} or n = {};
      then reconsider m = k \/ n as Element of omega by ORDINAL1:def 12;
      take m;
      thus m divides k & m divides n by A1,Th9;
      thus thesis by A1;
    end;
    suppose
A2:   k <> {} & n <> {};
      reconsider l = (k*^n) div^ (k lcm n) as Element of omega by
ORDINAL1:def 12;
      take l;
      thus l divides k & l divides n by A2,Th13;
      let m;
      assume that
A3:   m divides k and
A4:   m divides n;
A5:   n = m*^(n div^ m) by A4,Th7;
      then
A6:   n div^ m <> {} by A2,ORDINAL2:35;
      m*^(k div^ m)*^(n div^ m) = n*^(k div^ m) by A5,ORDINAL3:50;
      then
A7:   n divides m*^(k div^ m)*^(n div^ m) by Def3;
      set mm = m*^((k div^ m)*^(n div^ m));
A8:   mm = m*^(k div^ m)*^(n div^ m) by ORDINAL3:50;
A9:   k = m*^(k div^ m) by A3,Th7;
      then k div^ m <> {} by A2,ORDINAL2:35;
      then
A10:  (k div^ m)*^(n div^ m) <> {} by A6,ORDINAL3:31;
      k divides m*^(k div^ m)*^(n div^ m) by A9,Def3;
      then k lcm n divides m*^(k div^ m)*^(n div^ m) by A7,Def4;
      then
A11:  mm = (k lcm n)*^(mm div^ (k lcm n)) by A8,Th7;
      m <> {} by A2,A9,ORDINAL2:35;
      then k lcm n <> {} by A11,A10,ORDINAL2:35,ORDINAL3:31;
      then
A12:  k*^n = k*^n+^{} & {} in k lcm n by ORDINAL2:27,ORDINAL3:8;
      mm*^m = (k lcm n)*^(m*^(mm div^ (k lcm n))) by A11,ORDINAL3:50;
      then k*^n = (k lcm n)*^(m*^(mm div^ (k lcm n))) by A9,A5,A8,ORDINAL3:50;
      then l = m*^(mm div^ (k lcm n)) by A12,ORDINAL3:66;
      hence thesis by Def3;
    end;
  end;
  uniqueness
  proof
    let m1,m2 be Element of omega;
    assume m1 divides k & m1 divides n & ( for m st m divides k & m divides
n holds m divides m1)& m2 divides k &( m2 divides n & for m st m divides k & m
    divides n holds m divides m2 );
    then m1 divides m2 & m2 divides m1;
    hence thesis by Th8;
  end;
  commutativity;
end;

theorem Th14:
  a hcf {} = a & a lcm {} = {}
proof
  reconsider e = a, c = {} as Element of omega by ORDINAL1:def 12;
A1: for b st a divides b & {} divides b holds c divides b;
  ( for n st n divides a & n divides {} holds n divides e)& a divides c by Th9
;
  hence thesis by A1,Def4,Def5;
end;

theorem Th15:
  a hcf b = {} implies a = {}
proof
  a hcf b divides a by Def5;
  then a = (a hcf b)*^(a div^ (a hcf b)) by Th7;
  hence thesis by ORDINAL2:35;
end;

theorem Th16:
  a hcf a = a & a lcm a = a
proof
  reconsider c = a as Element of omega by ORDINAL1:def 12;
  for b st b divides a & b divides a holds b divides c;
  hence a hcf a = a by Def5;
  for b st a divides b & a divides b holds c divides b;
  hence thesis by Def4;
end;

theorem Th17:
  (a*^c) hcf (b*^c) = (a hcf b)*^c
proof
  per cases;
  suppose
A1: c = {};
    then
A2: (a hcf b)*^c = {} by ORDINAL2:35;
    a*^c = {} & b*^c = {} by A1,ORDINAL2:35;
    hence thesis by A2,Th16;
  end;
  suppose
A3: c <> {} & a <> {};
    reconsider d = (a hcf b)*^c as Element of omega by ORDINAL1:def 12;
    set e = ((a*^c) hcf (b*^c)) div^ d;
    a hcf b divides b by Def5;
    then b = (a hcf b)*^(b div^ (a hcf b)) by Th7;
    then b*^c = d*^(b div^ (a hcf b)) by ORDINAL3:50;
    then
A4: d divides b*^c by Def3;
    a hcf b divides a by Def5;
    then a = (a hcf b)*^(a div^ (a hcf b)) by Th7;
    then a*^c = d*^(a div^ (a hcf b)) by ORDINAL3:50;
    then d divides a*^c by Def3;
    then d divides (a*^c) hcf (b*^c) by A4,Def5;
    then
A5: (a*^c) hcf (b*^c) = d*^e by Th7
      .= (a hcf b)*^e*^c by ORDINAL3:50;
    then (a hcf b)*^e*^c divides b*^c by Def5;
    then (a hcf b)*^e*^c*^((b*^c)div^((a hcf b)*^e*^c)) = b*^c by Th7;
    then (a hcf b)*^e*^((b*^c)div^((a hcf b)*^e*^c))*^c = b*^c by ORDINAL3:50;
    then (a hcf b)*^e*^((b*^c)div^((a hcf b)*^e*^c)) = b by A3,ORDINAL3:33;
    then
A6: (a hcf b)*^e divides b by Def3;
    (a hcf b)*^e*^c divides a*^c by A5,Def5;
    then (a hcf b)*^e*^c*^((a*^c)div^((a hcf b)*^e*^c)) = a*^c by Th7;
    then (a hcf b)*^e*^((a*^c)div^((a hcf b)*^e*^c))*^c = a*^c by ORDINAL3:50;
    then (a hcf b)*^e*^((a*^c)div^((a hcf b)*^e*^c)) = a by A3,ORDINAL3:33;
    then (a hcf b)*^e divides a by Def3;
    then (a hcf b)*^e divides a hcf b by A6,Def5;
    then (a hcf b)*^e*^((a hcf b) div^ ((a hcf b)*^e)) = a hcf b by Th7;
    then (a hcf b)*^(e*^((a hcf b) div^ ((a hcf b)*^e))) = a hcf b by
ORDINAL3:50
      .= (a hcf b)*^1 by ORDINAL2:39;
    then a hcf b = {} or e*^((a hcf b) div^ ((a hcf b)*^e)) = 1 by ORDINAL3:33;
    then e = 1 by A3,Th15,ORDINAL3:37;
    hence thesis by A5,ORDINAL2:39;
  end;
  suppose
    a = {};
    then a hcf b = b & a*^c = {} by Th14,ORDINAL2:35;
    hence thesis by Th14;
  end;
end;

theorem Th18:
  b <> {} implies a hcf b <> {} & b div^ (a hcf b) <> {}
proof
  a hcf b divides b by Def5;
  then b = (a hcf b)*^(b div^ (a hcf b)) by Th7;
  hence thesis by ORDINAL2:35;
end;

theorem Th19:
  a <> {} or b <> {} implies a div^ (a hcf b), b div^ (a hcf b)
  are_relative_prime
proof
  assume
A1: a <> {} or b <> {};
  set ab = a hcf b;
A2: 1*^a = a & 1*^b = b by ORDINAL2:39;
  per cases;
  suppose
    a = {} or b = {};
    then ab = b & b div^ b = 1 or ab = a & a div^ a = 1 by A1,A2,Th14,
ORDINAL3:68;
    hence thesis by Th2;
  end;
  suppose
A3: a <> {} & b <> {};
    ab divides b by Def5;
    then
A4: b = ab*^(b div^ ab) by Th7;
    then
A5: b div^ ab <> {} by A3,ORDINAL2:35;
    let c,d1,d2 be Ordinal such that
A6: a div^ (a hcf b) = c *^ d1 and
A7: b div^ (a hcf b) = c *^ d2;
    ab divides a by Def5;
    then
A8: a = ab*^(a div^ ab) by Th7;
    then a div^ ab <> {} by A3,ORDINAL2:35;
    then reconsider c,d1,d2 as Element of omega by A6,A7,A5,ORDINAL3:75;
    b = ab*^c*^d2 by A4,A7,ORDINAL3:50;
    then
A9: ab*^c divides b by Def3;
    a = ab*^c*^d1 by A8,A6,ORDINAL3:50;
    then ab*^c divides a by Def3;
    then ab*^c divides ab by A9,Def5;
    then ab = (ab*^c)*^(ab div^ (ab*^c)) by Th7;
    then ab = ab*^(c*^(ab div^ (ab*^c))) by ORDINAL3:50;
    then
A10: ab*^1 = ab*^(c*^(ab div^ (ab*^c))) by ORDINAL2:39;
    ab <> {} by A3,A8,ORDINAL2:35;
    then 1 = c*^(ab div^ (ab*^c)) by A10,ORDINAL3:33;
    hence thesis by ORDINAL3:37;
  end;
end;

theorem Th20:
  a,b are_relative_prime iff a hcf b = 1
proof
  a hcf b divides b by Def5;
  then
A1: b = (a hcf b)*^(b div^ (a hcf b)) by Th7;
  a hcf b divides a by Def5;
  then a = (a hcf b)*^(a div^ (a hcf b)) by Th7;
  hence a,b are_relative_prime implies a hcf b = 1 by A1,Def2;
  assume
A2: a hcf b = 1;
  let c,d1,d2 be Ordinal such that
A3: a = c*^d1 & b = c*^d2;
  a <> {} or b <> {} by A2,Th14;
  then reconsider c as Element of omega by A3,ORDINAL3:75;
  c divides a & c divides b by A3,Def3;
  then c divides 1 by A2,Def5;
  then ex d st 1 = c*^d by Th5;
  hence thesis by ORDINAL3:37;
end;

definition
  let a,b be natural Ordinal;
  func RED(a,b) -> Element of omega equals
  a div^ (a hcf b);
  coherence by ORDINAL1:def 12;
end;

theorem Th21:
  RED(a,b)*^(a hcf b) = a
proof
  a hcf b divides a by Def5;
  hence thesis by Th7;
end;

theorem
  a <> {} or b <> {} implies RED(a,b), RED(b,a) are_relative_prime by Th19;

theorem Th23:
  a,b are_relative_prime implies RED(a,b) = a
proof
  assume a,b are_relative_prime;
  then a hcf b = 1 by Th20;
  hence thesis by ORDINAL3:71;
end;

theorem Th24:
  RED(a,1) = a & RED(1,a) = 1
proof
  a,1 are_relative_prime by Th2;
  then a hcf 1 = 1 by Th20;
  hence thesis by ORDINAL3:71;
end;

theorem
  b <> {} implies RED(b,a) <> {} by Th18;

theorem Th26:
  RED({},a) = {} & (a <> {} implies RED(a,{}) = 1)
proof
  thus RED({},a) = {} by ORDINAL3:70;
  assume
A1: a <> {};
  thus RED(a,{}) = a div^ a by Th14
    .= a*^1 div^ a by ORDINAL2:39
    .= 1 by A1,ORDINAL3:68;
end;

theorem Th27:
  a <> {} implies RED(a,a) = 1
proof
  assume
A1: a <> {};
  thus RED(a,a) = a div^ a by Th16
    .= a*^1 div^ a by ORDINAL2:39
    .= 1 by A1,ORDINAL3:68;
end;

theorem Th28:
  c <> {} implies RED(a*^c, b*^c) = RED(a, b)
proof
  assume
A1: c <> {};
  a <> {} implies a hcf b <> {} by Th18;
  then
A2: a <> {} implies (a hcf b)*^c <> {} by A1,ORDINAL3:31;
A3: RED({},b) = {} & {}*^((a hcf b)*^c) = {} by ORDINAL2:35,ORDINAL3:70;
A4: a hcf b divides a by Def5;
  thus RED(a*^c, b*^c) = (a*^c)div^((a hcf b)*^c) by Th17
    .= (((a div^(a hcf b))*^(a hcf b))*^c)div^((a hcf b)*^c) by A4,Th7
    .= (RED(a,b)*^((a hcf b)*^c))div^((a hcf b)*^c) by ORDINAL3:50
    .= RED(a, b) by A2,A3,ORDINAL3:68,70;
end;

set RATplus = {[a,b] where a,b is Element of omega: a,b are_relative_prime & b
<> {}};

1,1 are_relative_prime by Th2;

then [1,1] in RATplus;

then reconsider RATplus as non empty set;

Lm4: [a,b] in RATplus implies a,b are_relative_prime & b <> {}
proof
  assume [a,b] in RATplus;
  then consider c,d being Element of omega such that
A1: [a,b] = [c,d] and
A2: c,d are_relative_prime & d <> {};
  a = c by A1,XTUPLE_0:1;
  hence thesis by A1,A2,XTUPLE_0:1;
end;

begin :: Non negative rationals

reserve i,j,k for Element of omega;

definition
  func RAT+ equals
  ({[i,j]: i,j are_relative_prime & j <> {}} \ {[k,1]: not
  contradiction}) \/ omega;
  correctness;
end;

Lm5: omega c= RAT+ by XBOOLE_1:7;

reserve x,y,z for Element of RAT+;

registration
  cluster RAT+ -> non empty;
  coherence;
end;

registration
  cluster non empty ordinal for Element of RAT+;
  existence by Lm2,Lm5;
end;

theorem Th29:
  x in omega or ex i,j st x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1
proof
  assume not x in omega;
  then
A1: x in RATplus \ {[k,1]: not contradiction} by XBOOLE_0:def 3;
  then
A2: not x in {[k,1]: not contradiction} by XBOOLE_0:def 5;
  x in RATplus by A1;
  then consider a,b being Element of omega such that
A3: x = [a,b] & a,b are_relative_prime & b <> {};
  [a,1] in {[k,1]: not contradiction};
  hence thesis by A2,A3;
end;

theorem Th30:
  not ex i,j being set st [i,j] is Ordinal
proof
  given i,j being set such that
A1: [i,j] is Ordinal;
  {} in [i,j] by A1,ORDINAL3:8;
  hence thesis by TARSKI:def 2;
end;

theorem Th31:
  A in RAT+ implies A in omega
proof
  assume A in RAT+ & not A in omega;
  then ex i,j st A = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 by Th29;
  hence thesis by Th30;
end;

registration
  cluster -> natural for ordinal Element of RAT+;
  coherence
  proof
    let x be ordinal Element of RAT+;
    assume not x in omega;
    then
A1: ex i,j st x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 by Th29;
    then {} in x by ORDINAL3:8;
    hence thesis by A1,TARSKI:def 2;
  end;
end;

theorem Th32:
  not ex i,j being set st [i,j] in omega
proof
  given i,j being set such that
A1: [i,j] in omega;
  reconsider a = [i,j] as Element of omega by A1;
  {} in a by ORDINAL3:8;
  hence thesis by TARSKI:def 2;
end;

theorem Th33:
  [i,j] in RAT+ iff i,j are_relative_prime & j <> {} & j <> 1
proof
A1: not [i,j] in omega by Th32;
  hereby
    assume [i,j] in RAT+;
    then
A2: [i,j] in RATplus \ {[k,1]: not contradiction} by A1,XBOOLE_0:def 3;
    hence i,j are_relative_prime & j <> {} by Lm4;
    not [i,j] in {[k,1]: not contradiction} by A2,XBOOLE_0:def 5;
    hence j <> 1;
  end;
  assume i,j are_relative_prime & j <> {};
  then
A3: [i,j] in RATplus;
  assume j <> 1;
  then not ex k st [i,j] = [k,1] by XTUPLE_0:1;
  then not [i,j] in {[k,1]: not contradiction};
  then [i,j] in RATplus \ {[k,1]: not contradiction} by A3,XBOOLE_0:def 5;
  hence thesis by XBOOLE_0:def 3;
end;

definition
  let x be Element of RAT+;
  func numerator x -> Element of omega means
  :Def8:
  it = x if x in omega otherwise ex a st x = [it,a];
  existence
  proof
    thus x in omega implies ex a being Element of omega st a = x;
    assume not x in omega;
    then x in RATplus \ {[k,1]: not contradiction} by XBOOLE_0:def 3;
    then x in RATplus;
    then consider a,b being Element of omega such that
A1: x = [a,b] and
    a,b are_relative_prime and
    b <> {};
    take a,b;
    thus thesis by A1;
  end;
  correctness by XTUPLE_0:1;
  func denominator x -> Element of omega means
  : Def9:
  it = 1 if x in omega otherwise ex a st x = [a,it];
  existence
  proof
    thus x in omega implies ex a being Element of omega st a = 1;
    assume not x in omega;
    then x in RATplus \ {[k,1]: not contradiction} by XBOOLE_0:def 3;
    then x in RATplus;
    then consider a,b being Element of omega such that
A2: x = [a,b] and
    a,b are_relative_prime and
    b <> {};
    take b,a;
    thus thesis by A2;
  end;
  correctness by XTUPLE_0:1;
end;

theorem Th34:
  numerator x, denominator x are_relative_prime
proof
  per cases;
  suppose
    x in omega;
    then denominator x = 1 by Def9;
    hence thesis by Th2;
  end;
  suppose
A1: not x in omega;
    then consider i,j such that
A2: x = [i,j] and
A3: i,j are_relative_prime and
    j <> {} and
    j <> 1 by Th29;
    i = numerator x by A1,A2,Def8;
    hence thesis by A1,A2,A3,Def9;
  end;
end;

theorem Th35:
  denominator x <> {}
proof
  per cases;
  suppose
    x in omega;
    hence thesis by Def9;
  end;
  suppose
A1: not x in omega;
    then ex i,j st x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 by
Th29;
    hence thesis by A1,Def9;
  end;
end;

theorem Th36:
  not x in omega implies x = [numerator x, denominator x] & denominator x <> 1
proof
  assume
A1: not x in omega;
  then consider i,j such that
A2: x = [i,j] and
  i,j are_relative_prime and
  j <> {} and
A3: j <> 1 by Th29;
  i = numerator x by A1,A2,Def8;
  hence thesis by A1,A2,A3,Def9;
end;

theorem Th37:
  x <> {} iff numerator x <> {}
proof
  hereby
    assume that
A1: x <> {} and
A2: numerator x = {};
A3: not x in omega by A1,A2,Def8;
    then consider i,j such that
A4: x = [i,j] and
A5: i,j are_relative_prime and
    j <> {} and
A6: j <> 1 by Th29;
    i = {} by A2,A3,A4,Def8;
    hence contradiction by A5,A6,Th3;
  end;
  {} in omega by ORDINAL1:def 11;
  hence thesis by Def8;
end;

theorem
  x in omega iff denominator x = 1 by Def9,Th36;

definition
  let i,j be natural Ordinal;
  func i/j -> Element of RAT+ equals
  :Def10:
  {} if j = {}, RED(i,j) if RED(j,i
  ) = 1 otherwise [RED(i,j), RED(j,i)];
  coherence
  proof
A1: now
      assume j <> {};
      then RED(i,j), RED(j,i) are_relative_prime & RED(j,i) <> {} by Th18,Th19;
      hence RED(j,i) <> 1 implies [RED(i,j), RED(j,i)] in RAT+ by Th33;
    end;
    RED(i,j) in omega;
    hence thesis by A1,Lm1,Lm5;
  end;
  consistency by Th26;
end;

notation
  let i,j be natural Ordinal;
  synonym quotient(i,j) for i/j;
end;

theorem Th39:
  (numerator x)/(denominator x) = x
proof
A1: denominator x <> {} by Th35;
A2: RED(numerator x, denominator x) = numerator x by Th23,Th34;
  numerator x, denominator x are_relative_prime by Th34;
  then
A3: RED(denominator x, numerator x) = denominator x by Th23;
  per cases;
  suppose
A4: denominator x = 1;
    then x in omega by Th36;
    then numerator x = x by Def8;
    hence thesis by A2,A3,A4,Def10;
  end;
  suppose
A5: denominator x <> 1;
    then not x in omega by Def9;
    then x = [numerator x, denominator x] by Th36;
    hence thesis by A1,A2,A3,A5,Def10;
  end;
end;

theorem Th40:
  {}/b = {} & a/1 = a
proof
A1: b <> {} implies RED(b,{}) = 1 by Th26;
  RED({},b) = {} by Th26;
  hence {}/b = {} by A1,Def10;
  RED(1,a) = 1 & RED(a,1) = a by Th24;
  hence thesis by Def10;
end;

theorem Th41:
  a <> {} implies a/a = 1
proof
  assume a <> {};
  then RED(a,a) = 1 by Th27;
  hence thesis by Def10;
end;

theorem Th42:
  b <> {} implies numerator (a/b) = RED(a,b) & denominator (a/b) = RED(b,a)
proof
  assume
A1: b <> {};
  per cases;
  suppose
A2: RED(b,a) = 1;
    then a/b = RED(a,b) by Def10;
    hence thesis by A2,Def8,Def9;
  end;
  suppose
A3: RED(b,a) <> 1;
A4: not [RED(a,b), RED(b,a)] in omega by Th32;
    a/b = [RED(a,b), RED(b,a)] by A1,A3,Def10;
    hence thesis by A4,Def8,Def9;
  end;
end;

theorem Th43:
  i,j are_relative_prime & j <> {} implies numerator (i/j) = i &
  denominator (i/j) = j
proof
  assume i,j are_relative_prime;
  then RED(i,j) = i & RED(j,i) = j by Th23;
  hence thesis by Th42;
end;

theorem Th44:
  c <> {} implies (a*^c)/(b*^c) = a/b
proof
  assume
A1: c <> {};
  per cases;
  suppose
    b = {};
    then a/b = {} & b*^c = {} by Def10,ORDINAL2:35;
    hence thesis by Def10;
  end;
  suppose
A2: b <> {};
    then
A3: b*^c <> {} by A1,ORDINAL3:31;
    then
A4: denominator ((a*^c)/(b*^c)) = RED(b*^c,a*^c) by Th42
      .= RED(b,a) by A1,Th28
      .= denominator (a/b) by A2,Th42;
    numerator ((a*^c)/(b*^c)) = RED(a*^c,b*^c) by A3,Th42
      .= RED(a,b) by A1,Th28
      .= numerator (a/b) by A2,Th42;
    hence (a*^c)/(b*^c) = (numerator (a/b))/denominator (a/b) by A4,Th39
      .= a/b by Th39;
  end;
end;

reserve i,j,k for natural Ordinal;

theorem Th45:
  j <> {} & l <> {} implies (i/j = k/l iff i*^l = j*^k)
proof
  assume that
A1: j <> {} and
A2: l <> {};
  set x = i/j, y = k/l;
  set ny = numerator y, dy = denominator y;
A3: ny = RED(k,l) by A2,Th42;
  set nx = numerator x, dx = denominator x;
A4: dx = RED(j,i) by A1,Th42;
A5: dy = RED(l,k) by A2,Th42;
A6: nx = RED(i,j) by A1,Th42;
  hereby
    assume i/j = k/l;
    then i = ny*^(i hcf j) & l = dx*^(l hcf k) by A6,A5,Th21;
    hence i*^l = ny*^(i hcf j)*^dx*^(l hcf k) by ORDINAL3:50
      .= ny*^((i hcf j)*^dx)*^(l hcf k) by ORDINAL3:50
      .= ny*^j*^(l hcf k) by A4,Th21
      .= j*^(ny*^(l hcf k)) by ORDINAL3:50
      .= j*^k by A3,Th21;
  end;
  assume
A7: i*^l = j*^k;
  then dx = RED(j*^l,j*^k) by A2,A4,Th28;
  then
A8: dx = dy by A1,A5,Th28;
  nx = RED(j*^k,j*^l) by A2,A6,A7,Th28;
  then nx = ny by A1,A3,Th28;
  then x = ny/dy by A8,Th39;
  hence thesis by Th39;
end;

definition
  let x,y be Element of RAT+;
  func x+y -> Element of RAT+ equals
  ((numerator x)*^(denominator y)+^(
  numerator y)*^(denominator x)) / ((denominator x)*^(denominator y));
  coherence;
  commutativity;
  func x*'y -> Element of RAT+ equals
  ((numerator x)*^(numerator y)) / ((
  denominator x)*^(denominator y));
  coherence;
  commutativity;
end;

theorem Th46:
  j <> {} & l <> {} implies (i/j)+(k/l) = (i*^l+^j*^k)/(j*^l)
proof
  assume that
A1: j <> {} and
A2: l <> {};
A3: denominator (k/l) = RED(l,k) & denominator (i/j) = RED(j,i) by A1,A2,Th42;
  numerator (k/l) = RED(k,l) & numerator (i/j) = RED(i,j) by A1,A2,Th42;
  hence
  (i/j)+(k/l) = (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))*^(i hcf j) /(RED
  (j,i)*^RED(l,k)*^(i hcf j)) by A1,A3,Th15,Th44
    .= (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))*^(i hcf j) /(RED(l,k)*^(RED(
  j,i)*^(i hcf j))) by ORDINAL3:50
    .= (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))*^(i hcf j)/(RED(l,k)*^j) by
Th21
    .= (RED(i,j)*^RED(l,k)*^(i hcf j)+^RED(j,i)*^RED(k,l)*^(i hcf j)) /(RED(
  l,k)*^j) by ORDINAL3:46
    .= (RED(l,k)*^(RED(i,j)*^(i hcf j))+^RED(j,i)*^RED(k,l)*^(i hcf j)) /(
  RED(l,k)*^j) by ORDINAL3:50
    .= (RED(l,k)*^i+^RED(j,i)*^RED(k,l)*^(i hcf j))/(RED(l,k)*^j) by Th21
    .= (RED(l,k)*^i+^RED(k,l)*^(RED(j,i)*^(i hcf j)))/(RED(l,k)*^j) by
ORDINAL3:50
    .= (RED(l,k)*^i+^RED(k,l)*^j)/(RED(l,k)*^j) by Th21
    .= ((RED(l,k)*^i+^RED(k,l)*^j)*^(k hcf l))/(RED(l,k)*^j*^(k hcf l)) by A2
,Th15,Th44
    .= ((RED(l,k)*^i+^RED(k,l)*^j)*^(k hcf l))/(j*^(RED(l,k)*^(k hcf l))) by
ORDINAL3:50
    .= ((RED(l,k)*^i+^RED(k,l)*^j)*^(k hcf l))/(j*^l) by Th21
    .= (RED(l,k)*^i*^(k hcf l)+^RED(k,l)*^j*^(k hcf l))/(j*^l) by ORDINAL3:46
    .= (i*^(RED(l,k)*^(k hcf l))+^RED(k,l)*^j*^(k hcf l))/(j*^l) by ORDINAL3:50
    .= (i*^l+^RED(k,l)*^j*^(k hcf l))/(j*^l) by Th21
    .= (i*^l+^j*^(RED(k,l)*^(k hcf l)))/(j*^l) by ORDINAL3:50
    .= (i*^l+^j*^k)/(j*^l) by Th21;
end;

theorem Th47:
  k <> {} implies (i/k)+(j/k) = (i+^j)/k
proof
  assume
A1: k <> {};
  hence (i/k)+(j/k) = (i*^k+^j*^k)/(k*^k) by Th46
    .= ((i+^j)*^k)/(k*^k) by ORDINAL3:46
    .= (i+^j)/k by A1,Th44;
end;

registration
  cluster empty for Element of RAT+;
  existence by Lm1,Lm5;
end;

definition
  redefine func {} -> Element of RAT+;
  coherence by Lm1,Lm5;
  redefine func one -> non empty ordinal Element of RAT+;
  coherence by Lm2,Lm5;
end;

theorem Th48:
  x*'{} = {}
proof
  numerator {} = {} & (numerator x)*^{} = {} by Def8,Lm1,ORDINAL2:35;
  hence thesis by Th40;
end;

theorem Th49:
  (i/j)*'(k/l) = (i*^k)/(j*^l)
proof
  per cases;
  suppose
A1: j <> {} & l <> {};
    then
A2: denominator (k/l) = RED(l,k) & denominator (i/j) = RED(j,i) by Th42;
    numerator (k/l) = RED(k,l) & numerator (i/j) = RED(i,j) by A1,Th42;
    hence
    (i/j)*'(k/l) = (RED(i,j)*^RED(k,l)*^(i hcf j))/(RED(j,i)*^RED(l,k)*^(
    i hcf j)) by A1,A2,Th15,Th44
      .= (RED(k,l)*^(RED(i,j)*^(i hcf j)))/(RED(j,i)*^RED(l,k)*^(i hcf j))
    by ORDINAL3:50
      .= (RED(k,l)*^i)/(RED(j,i)*^RED(l,k)*^(i hcf j)) by Th21
      .= (RED(k,l)*^i)/(RED(l,k)*^(RED(j,i)*^(i hcf j))) by ORDINAL3:50
      .= (RED(k,l)*^i)/(RED(l,k)*^j) by Th21
      .= (RED(k,l)*^i*^(l hcf k))/(RED(l,k)*^j*^(l hcf k)) by A1,Th15,Th44
      .= (i*^(RED(k,l)*^(l hcf k)))/(RED(l,k)*^j*^(l hcf k)) by ORDINAL3:50
      .= (i*^k)/(RED(l,k)*^j*^(l hcf k)) by Th21
      .= (i*^k)/(j*^(RED(l,k)*^(l hcf k))) by ORDINAL3:50
      .= (i*^k)/(j*^l) by Th21;
  end;
  suppose
A3: j = {} or l = {};
    then i/j = {} or k/l = {} by Def10;
    then
A4: (i/j)*'(k/l) = {} by Th48;
    j*^l = {} by A3,ORDINAL2:35;
    hence thesis by A4,Def10;
  end;
end;

theorem Th50:
  x+{} = x
proof
A1: (numerator x)*^1 = numerator x & {}*^(denominator x) = {} by ORDINAL2:35,39
;
A2: (denominator x)*^1 = denominator x & (numerator x)+^{} = numerator x by
ORDINAL2:27,39;
  denominator {} = 1 & numerator {} = {} by Def8,Def9,Lm1;
  hence thesis by A1,A2,Th39;
end;

theorem Th51:
  (x+y)+z = x+(y+z)
proof
  set nx = numerator x, ny = numerator y, nz = numerator z;
  set dx = denominator x, dy = denominator y, dz = denominator z;
A1: dy <> {} by Th35;
A2: dz <> {} by Th35;
  then
A3: dy*^dz <> {} by A1,ORDINAL3:31;
A4: dx <> {} by Th35;
  then
A5: dx*^dy <> {} by A1,ORDINAL3:31;
  thus x+y+z = (nx*^dy+^dx*^ny)/(dx*^dy)+nz/dz by Th39
    .= ((nx*^dy+^dx*^ny)*^dz+^(dx*^dy)*^nz)/(dx*^dy*^dz) by A2,A5,Th46
    .= (nx*^dy*^dz+^dx*^ny*^dz+^dx*^dy*^nz)/(dx*^dy*^dz) by ORDINAL3:46
    .= (nx*^(dy*^dz)+^dx*^ny*^dz+^dx*^dy*^nz)/(dx*^dy*^dz) by ORDINAL3:50
    .= (nx*^(dy*^dz)+^dx*^(ny*^dz)+^dx*^dy*^nz)/(dx*^dy*^dz) by ORDINAL3:50
    .= (nx*^(dy*^dz)+^dx*^(ny*^dz)+^dx*^(dy*^nz))/(dx*^dy*^dz) by ORDINAL3:50
    .= (nx*^(dy*^dz)+^(dx*^(ny*^dz)+^dx*^(dy*^nz)))/(dx*^dy*^dz) by ORDINAL3:30
    .= (nx*^(dy*^dz)+^dx*^(ny*^dz+^dy*^nz))/(dx*^dy*^dz) by ORDINAL3:46
    .= (nx*^(dy*^dz)+^dx*^(ny*^dz+^dy*^nz))/(dx*^(dy*^dz)) by ORDINAL3:50
    .= (ny*^dz+^dy*^nz)/(dy*^dz)+nx/dx by A4,A3,Th46
    .= x+(y+z) by Th39;
end;

theorem Th52:
  (x*'y)*'z = x*'(y*'z)
proof
  set nx = numerator x, ny = numerator y, nz = numerator z;
  set dx = denominator x, dy = denominator y, dz = denominator z;
A1: x = nx/dx by Th39;
  z = nz/dz by Th39;
  hence (x*'y)*'z = (nx*^ny*^nz)/(dx*^dy*^dz) by Th49
    .= (nx*^(ny*^nz))/(dx*^dy*^dz) by ORDINAL3:50
    .= (nx*^(ny*^nz))/(dx*^(dy*^dz)) by ORDINAL3:50
    .= x*'(y*'z) by A1,Th49;
end;

theorem Th53:
  x*'one = x
proof
  set y = one;
A1: (numerator x)*^1 = numerator x & (denominator x)*^1 = denominator x by
ORDINAL2:39;
  numerator y = 1 & denominator y = 1 by Def8,Def9;
  hence thesis by A1,Th39;
end;

theorem Th54:
  x <> {} implies ex y st x*'y = 1
proof
  set nx = numerator x, dx = denominator x;
A1: dx <> {} by Th35;
  assume x <> {};
  then
A2: nx <> {} by Th37;
  take y = dx/nx;
  nx, dx are_relative_prime by Th34;
  then denominator y = nx & numerator y = dx by A2,Th43;
  hence thesis by A2,A1,Th41,ORDINAL3:31;
end;

theorem Th55:
  x <> {} implies ex z st y = x*'z
proof
  reconsider o = one as Element of RAT+;
  assume x <> {};
  then consider z such that
A1: x*'z = 1 by Th54;
  take z*'y;
  thus y = y*'o by Th53
    .= x*'(z*'y) by A1,Th52;
end;

theorem Th56:
  x <> {} & x*'y = x*'z implies y = z
proof
  assume x <> {};
  then consider r being Element of RAT+ such that
A1: x*'r = 1 by Th54;
  r*'(x*'y) = one*'y by A1,Th52;
  then
A2: r*'(x*'y) = y by Th53;
  r*'(x*'z) = one*'z by A1,Th52;
  hence thesis by A2,Th53;
end;

theorem Th57:
  x*'(y+z) = x*'y+x*'z
proof
  set nx = numerator x, ny = numerator y, nz = numerator z;
  set dx = denominator x, dy = denominator y, dz = denominator z;
A1: dx <> {} by Th35;
  dz <> {} by Th35;
  then
A2: dx*^dz <> {} by A1,ORDINAL3:31;
  dy <> {} by Th35;
  then
A3: dx*^dy <> {} by A1,ORDINAL3:31;
  x = nx/dx by Th39;
  hence x*'(y+z) = (nx*^(ny*^dz+^dy*^nz))/(dx*^(dy*^dz)) by Th49
    .= (nx*^(ny*^dz)+^nx*^(dy*^nz))/(dx*^(dy*^dz)) by ORDINAL3:46
    .= (nx*^ny*^dz+^nx*^(dy*^nz))/(dx*^(dy*^dz)) by ORDINAL3:50
    .= (nx*^ny*^dz+^dy*^(nx*^nz))/(dx*^(dy*^dz)) by ORDINAL3:50
    .= (nx*^ny*^dz+^dy*^(nx*^nz))/(dy*^(dx*^dz)) by ORDINAL3:50
    .= (dx*^((nx*^ny)*^dz+^(dy*^(nx*^nz))))/(dx*^(dy*^(dx*^dz))) by Th35,Th44
    .= (dx*^((nx*^ny)*^dz)+^dx*^(dy*^(nx*^nz)))/(dx*^(dy*^(dx*^dz))) by
ORDINAL3:46
    .= (dx*^((nx*^ny)*^dz)+^(dx*^dy)*^(nx*^nz))/(dx*^(dy*^(dx*^dz))) by
ORDINAL3:50
    .= ((nx*^ny)*^(dx*^dz)+^(dx*^dy)*^(nx*^nz))/(dx*^(dy*^(dx*^dz))) by
ORDINAL3:50
    .= ((nx*^ny)*^(dx*^dz)+^(dx*^dy)*^(nx*^nz))/((dx*^dy)*^(dx*^dz)) by
ORDINAL3:50
    .= x*'y+x*'z by A2,A3,Th46;
end;

theorem Th58:
  for i,j being ordinal Element of RAT+ holds i+j = i+^j
proof
  let i,j be ordinal Element of RAT+;
  set ni = numerator i, nj = numerator j;
A1: j in omega by ORDINAL1:def 12;
  then
A2: denominator j = 1 by Def9;
A3: i in omega by ORDINAL1:def 12;
  then denominator i = 1 by Def9;
  hence i+j = (ni*^1+^1*^nj)/1 by A2,ORDINAL2:39
    .= (ni+^1*^nj)/1 by ORDINAL2:39
    .= (ni+^nj)/1 by ORDINAL2:39
    .= ni+^nj by Th40
    .= i+^nj by A3,Def8
    .= i+^j by A1,Def8;
end;

theorem
  for i,j being ordinal Element of RAT+ holds i*'j = i*^j
proof
  let i,j be ordinal Element of RAT+;
  set ni = numerator i, nj = numerator j;
A1: j in omega by ORDINAL1:def 12;
  then
A2: denominator j = 1 by Def9;
A3: i in omega by ORDINAL1:def 12;
  then denominator i = 1 by Def9;
  hence i*'j = (ni*^nj)/1 by A2,ORDINAL2:39
    .= ni*^nj by Th40
    .= i*^nj by A3,Def8
    .= i*^j by A1,Def8;
end;

theorem Th60:
  ex y st x = y+y
proof
  set 02 = one+one;
  02 = 1+^1 by Th58;
  then 02 <> {} by ORDINAL3:26;
  then consider z such that
A1: 02*'z = 1 by Th54;
  take y = z*'x;
  thus x = one*'x by Th53
    .= 02*'y by A1,Th52
    .= one*'y+one*'y by Th57
    .= y+one*'y by Th53
    .= y+y by Th53;
end;

definition
  let x,y be Element of RAT+;
  pred x <=' y means
  : Def13:
  ex z being Element of RAT+ st y = x+z;
  connectedness
  proof
    let x,y be Element of RAT+;
    set nx = numerator x, ny = numerator y;
    set dx = denominator x, dy = denominator y;
A1: dx <> {} & dy <> {} by Th35;
A2: nx/dx = x & ny/dy = y by Th39;
    nx*^dy c= ny*^dx or ny*^dx c= nx*^dy;
    then
A3: ny*^dx = nx*^dy+^(ny*^dx -^ nx*^dy) or nx*^dy = ny*^dx+^(nx*^dy -^ ny
    *^dx) by ORDINAL3:def 5;
    nx*^dy/(dx*^dy) = nx/dx & ny*^dx/(dx*^dy) = ny/dy by Th35,Th44;
    then x = y+((nx*^dy -^ ny*^dx)/(dx*^dy)) or y = x+((ny*^dx -^ nx*^dy)/(dx
    *^dy)) by A1,A2,A3,Th47,ORDINAL3:31;
    hence thesis;
  end;
end;

notation
  let x,y be Element of RAT+;
  antonym y < x for x <=' y;
end;

reserve r,s,t for Element of RAT+;

theorem
  not ex y being set st [{},y] in RAT+
proof
  given y being set such that
A1: [{},y] in RAT+;
  consider i,j being Element of omega such that
A2: [{},y] = [i,j] and
A3: i,j are_relative_prime and
  j <> {} and
A4: j <> 1 by A1,Th29,Th32;
  i = {} by A2,XTUPLE_0:1;
  hence thesis by A3,A4,Th3;
end;

theorem Th62:
  s + t = r + t implies s = r
proof
  assume
A1: s + t = r + t;
  set r1 = numerator r, r2 = denominator r;
  set t1 = numerator t, t2 = denominator t;
  set s1 = numerator s, s2 = denominator s;
A2: t2 <> {} by Th35;
A3: s2 <> {} by Th35;
  then
A4: s2*^t2 <> {} by A2,ORDINAL3:31;
A5: r2 <> {} by Th35;
  then r2*^t2 <> {} by A2,ORDINAL3:31;
  then (s1*^t2+^s2*^t1)*^(r2*^t2) = (r1*^t2+^r2*^t1)*^(s2*^t2) by A1,A4,Th45
    .= (r1*^t2+^r2*^t1)*^s2*^t2 by ORDINAL3:50;
  then (s1*^t2+^s2*^t1)*^r2*^t2 = (r1*^t2+^r2*^t1)*^s2*^t2 by ORDINAL3:50;
  then (s1*^t2+^s2*^t1)*^r2 = (r1*^t2+^r2*^t1)*^s2 by A2,ORDINAL3:33
    .= r1*^t2*^s2+^r2*^t1*^s2 by ORDINAL3:46;
  then s1*^t2*^r2+^s2*^t1*^r2 = r1*^t2*^s2+^r2*^t1*^s2 by ORDINAL3:46
    .= r1*^t2*^s2+^s2*^t1*^r2 by ORDINAL3:50;
  then s1*^t2*^r2 = r1*^t2*^s2 by ORDINAL3:21
    .= r1*^s2*^t2 by ORDINAL3:50;
  then s1*^r2*^t2 = r1*^s2*^t2 by ORDINAL3:50;
  then s1*^r2 = r1*^s2 by A2,ORDINAL3:33;
  then s1/s2 = r1/r2 by A3,A5,Th45
    .= r by Th39;
  hence thesis by Th39;
end;

theorem Th63:
  r+s = {} implies r = {}
proof
  set nr = numerator r, dr = denominator r;
  set ns = numerator s, ds = denominator s;
  assume
A1: r+s = {};
  denominator {} = 1 & numerator {} = {} by Def8,Def9,Lm1;
  then
A2: (nr*^ds+^ns*^dr)/(dr*^ds) = {}/1 by A1,Th39;
A3: ds <> {} by Th35;
  dr <> {} by Th35;
  then dr*^ds <> {} by A3,ORDINAL3:31;
  then (nr*^ds+^ns*^dr)*^1 = (dr*^ds)*^{} by A2,Th45
    .= {} by ORDINAL2:35;
  then nr*^ds+^ns*^dr = {} by ORDINAL3:31;
  then nr*^ds = {} by ORDINAL3:26;
  then nr = {} by A3,ORDINAL3:31;
  hence thesis by Th37;
end;

theorem Th64:
  {} <=' s
proof
  take s;
  thus thesis by Th50;
end;

theorem
  s <=' {} implies s = {}
proof
  assume ex r st {} = s+r;
  hence thesis by Th63;
end;

theorem Th66:
  r <=' s & s <=' r implies r = s
proof
  given x such that
A1: s = r+x;
  given y such that
A2: r = s+y;
  r+{} = r by Th50
    .= r+(x+y) by A1,A2,Th51;
  then x = {} by Th62,Th63;
  hence thesis by A1,Th50;
end;

theorem Th67:
  r <=' s & s <=' t implies r <=' t
proof
  given x such that
A1: s = r+x;
  given y such that
A2: t = s+y;
  take x+y;
  thus thesis by A1,A2,Th51;
end;

theorem
  r < s iff r <=' s & r <> s by Th66;

theorem
  r < s & s <=' t or r <=' s & s < t implies r < t by Th67;

theorem
  r < s & s < t implies r < t by Th67;

theorem Th71:
  x in omega & x+y in omega implies y in omega
proof
  assume that
A1: x in omega and
A2: x+y in omega;
A3: denominator (x+y) = 1 by A2,Def9;
  set nx = numerator x, dx = denominator x;
A4: dx = 1 by A1,Def9;
  set ny = numerator y, dy = denominator y;
A5: x+y = numerator (x+y)/denominator (x+y) & (nx*^dy+^ny*^dx)*^1 = nx*^dy+^
  ny*^ dx by Th39,ORDINAL2:39;
  dy <> {} by Th35;
  then dx*^dy <> {} by A4,ORDINAL3:31;
  then nx*^dy+^ny*^dx = dx*^dy*^numerator (x+y) by A3,A5,Th45
    .= dy*^numerator (x+y) by A4,ORDINAL2:39;
  then nx*^dy+^ny = dy*^numerator (x+y) by A4,ORDINAL2:39;
  then ny = (dy*^numerator (x+y))-^nx*^dy by ORDINAL3:52;
  then ny = dy*^((numerator (x+y))-^nx) by ORDINAL3:63;
  then
A6: dy divides ny by Def3;
A7: ny,dy are_relative_prime by Th34;
  for m being natural Ordinal st m divides dy & m divides ny holds m
  divides dy;
  then dy hcf ny = dy by A6,Def5;
  then
A8: dy = 1 by A7,Th20;
  y = ny/dy by Th39;
  then y = ny by A8,Th40;
  hence thesis;
end;

theorem Th72:
  for i being ordinal Element of RAT+ st i < x & x < i+one holds not x in omega
proof
  let i be ordinal Element of RAT+;
  assume that
A1: i < x and
A2: x < i+one and
A3: x in omega;
  consider z such that
A4: i+one = x+z by A2,Def13;
  i+one = i+^1 by Th58;
  then i+one in omega by Th31;
  then reconsider z9 = z as Element of omega by A3,A4,Th71;
  consider y such that
A5: x = i+y by A1,Def13;
  i in omega by Th31;
  then reconsider y9 = y as Element of omega by A3,A5,Th71;
  i+one = i+(y+z) by A5,A4,Th51;
  then 1 = y+z by Th62
    .= y9+^z9 by Th58;
  then y9 c= 1 by ORDINAL3:24;
  then y = {} or y = 1 by ORDINAL3:16;
  then i = x or i+one = x by A5,Th50;
  hence contradiction by A1,A2;
end;

theorem Th73:
  t <> {} implies ex r st r < t & not r in omega
proof
  assume
A1: t <> {};
A2: 1+^1 = succ 1 by ORDINAL2:31;
  per cases;
  suppose
A3: one <=' t;
    consider r such that
A4: one = r+r by Th60;
    take r;
    r <=' one & r <> 1 by A2,A4,Def13,Th58;
    then r < one by Th66;
    hence r < t by A3,Th67;
A5: 1*^1 = 1 by ORDINAL2:39;
    assume r in omega;
    then
A6: denominator r = 1 by Def9;
    then (numerator r)*^denominator r = numerator r by ORDINAL2:39;
    then
A7: 1 = (numerator r)+^numerator r by A4,A6,A5,Th40;
    then numerator r c= 1 by ORDINAL3:24;
    then numerator r = {} or numerator r = 1 by ORDINAL3:16;
    hence contradiction by A2,A7,ORDINAL2:27;
  end;
  suppose
A8: t < one;
    consider r such that
A9: t = r+r by Th60;
A10: {} <=' r by Th64;
    r <> {} by A1,A9,Th50;
    then
A11: {} < r by A10,Th66;
    take r;
A12: 1 = {}+one by Th50;
A13: r <=' t by A9,Def13;
    now
      assume r = t;
      then t+{} = t+t by A9,Th50;
      hence contradiction by A1,Th62;
    end;
    hence r < t by A13,Th66;
    r < one by A8,A13,Th67;
    hence thesis by A11,A12,Th72;
  end;
end;

theorem
  {s: s < t} in RAT+ iff t = {}
proof
  hereby
    assume
A1: {s: s < t} in RAT+ & t <> {};
    then consider r such that
A2: r < t and
A3: not r in omega by Th73;
    {} <=' t by Th64;
    then {} < t by A1,Th66;
    then
A4: {} in {s: s < t};
    r in {s: s < t} by A2;
    then {s: s < t} in omega implies r is Ordinal;
    then ex i,j being Element of omega st {s: s < t} = [i,j] & i,j
    are_relative_prime & j <> {} & j <> 1 by A1,A3,Th29,Th31;
    hence contradiction by A4,TARSKI:def 2;
  end;
  assume
A5: t = {};
  {s: s < t} c= {}
  proof
    let a be set;
    assume a in {s: s < t};
    then ex s st a = s & s < t;
    hence thesis by A5,Th64;
  end;
  then {s: s < t} = {};
  hence thesis;
end;

theorem
  for A being Subset of RAT+ st (ex t st t in A & t <> {}) & for r,s st
r in A & s <=' r holds s in A ex r1,r2,r3 being Element of RAT+ st r1 in A & r2
  in A & r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1
proof
  let A be Subset of RAT+;
  given t such that
A1: t in A and
A2: t <> {};
  assume
A3: for r,s st r in A & s <=' r holds s in A;
  consider x such that
A4: t = x+x by Th60;
  take {}, x, t;
  x <=' t by A4,Def13;
  hence {} in A & x in A & t in A by A1,A3,Th64;
  thus {} <> x by A2,A4,Th50;
  hereby
    assume x = t;
    then t+{} = t+t by A4,Th50;
    hence contradiction by A2,Th62;
  end;
  thus thesis by A2;
end;

theorem Th76:
  s + t <=' r + t iff s <=' r
proof
  thus s + t <=' r + t implies s <=' r
  proof
    given z such that
A1: r+t = s+t+z;
    take z;
    r+t = s+z+t by A1,Th51;
    hence thesis by Th62;
  end;
  given z such that
A2: r = s+z;
  take z;
  thus thesis by A2,Th51;
end;

theorem
  s <=' s + t
proof
  take t;
  thus thesis;
end;

theorem
  r*'s = {} implies r = {} or s = {}
proof
  set nr = numerator r, dr = denominator r;
  set ns = numerator s, ds = denominator s;
  assume
A1: r*'s = {};
  dr <> {} & ds <> {} by Th35;
  then
A2: dr*^ds <> {} by ORDINAL3:31;
  denominator {} = 1 & numerator {} = {} by Def8,Def9,Lm1;
  then (nr*^ns)/(dr*^ds) = {}/1 by A1,Th39;
  then (nr*^ns)*^1 = (dr*^ds)*^{} by A2,Th45
    .= {} by ORDINAL2:35;
  then nr*^ns = {} by ORDINAL3:31;
  then nr = {} or ns = {} by ORDINAL3:31;
  hence thesis by Th37;
end;

theorem Th79:
  r <=' s *' t implies ex t0 being Element of RAT+ st r = s *' t0 & t0 <=' t
proof
  given x such that
A1: s*'t = r+x;
  per cases;
  suppose
A2: s = {};
    take t;
    s*'t = {} by A2,Th48;
    hence thesis by A1,Th63;
  end;
  suppose
A3: s <> {};
    then consider t1 being Element of RAT+ such that
A4: x = s*'t1 by Th55;
    consider t0 being Element of RAT+ such that
A5: r = s*'t0 by A3,Th55;
    take t0;
    thus r = s*'t0 by A5;
    take t1;
    s*'t = s*'(t0+t1) by A1,A5,A4,Th57;
    hence thesis by A3,Th56;
  end;
end;

theorem
  t <> {} & s *' t <=' r *' t implies s <=' r
proof
  assume that
A1: t <> {} and
A2: s *' t <=' r *' t;
  ex x st s*'t = t*'x & x <=' r by A2,Th79;
  hence thesis by A1,Th56;
end;

theorem
  for r1,r2,s1,s2 being Element of RAT+ st r1+r2 = s1+s2 holds r1 <=' s1
  or r2 <=' s2
proof
  let r1,r2,s1,s2 be Element of RAT+ such that
A1: r1+r2 = s1+s2;
  assume that
A2: s1 < r1 and
A3: s2 < r2;
  s1+s2 < r1+s2 by A2,Th76;
  hence thesis by A1,A3,Th76;
end;

theorem Th82:
  s <=' r implies s *' t <=' r *' t
proof
  given x such that
A1: r = s+x;
  take x*'t;
  thus thesis by A1,Th57;
end;

theorem
  for r1,r2,s1,s2 being Element of RAT+ st r1*'r2 = s1*'s2 holds r1 <='
  s1 or r2 <=' s2
proof
  let r1,r2,s1,s2 be Element of RAT+ such that
A1: r1*'r2 = s1*'s2;
A2: {} <=' s1 by Th64;
  assume that
A3: s1 < r1 and
A4: s2 < r2;
  s2 <> r2 & s1*'s2 <=' r1*'s2 by A3,A4,Th82;
  then s1*'s2 < r1*'s2 by A1,A3,A2,Th56,Th66;
  hence thesis by A1,A4,Th82;
end;

theorem
  r = {} iff r + s = s
proof
  s+{} = s by Th50;
  hence thesis by Th62;
end;

theorem
  for s1,t1,s2,t2 being Element of RAT+ st s1 + t1 = s2 + t2 & s1 <=' s2
  holds t2 <=' t1
proof
  let s1,t1,s2,t2 be Element of RAT+ such that
A1: s1 + t1 = s2 + t2;
  given x such that
A2: s2 = s1+x;
  take x;
  s1+t1 = s1+(x+t2) by A1,A2,Th51;
  hence thesis by Th62;
end;

theorem Th86:
  r <=' s & s <=' r + t implies ex t0 being Element of RAT+ st s =
  r + t0 & t0 <=' t
proof
  given t0 being Element of RAT+ such that
A1: s = r+t0;
  assume s <=' r+t;
  then t0 <=' t by A1,Th76;
  hence thesis by A1;
end;

theorem
  r <=' s + t implies ex s0,t0 being Element of RAT+ st r = s0 + t0 & s0
  <=' s & t0 <=' t
proof
  assume
A1: r <=' s + t;
  per cases;
  suppose
    s <=' r;
    then
    s <=' s & ex t0 being Element of RAT+ st r = s + t0 & t0 <=' t by A1,Th86;
    hence thesis;
  end;
  suppose
A2: r <=' s;
    r = r+{} & {} <=' t by Th50,Th64;
    hence thesis by A2;
  end;
end;

theorem
  r < s & r < t implies ex t0 being Element of RAT+ st t0 <=' s & t0 <='
  t & r < t0
proof
  s <=' t & s <=' s or t <=' s & t <=' t;
  hence thesis;
end;

theorem
  r <=' s & s <=' t & s <> t implies r <> t by Th66;

theorem
  s < r + t & t <> {} implies ex r0,t0 being Element of RAT+ st s = r0 +
  t0 & r0 <=' r & t0 <=' t & t0 <> t
proof
  assume that
A1: s < r + t and
A2: t <> {};
  per cases;
  suppose
    r <=' s;
    then consider t0 being Element of RAT+ such that
A3: s = r + t0 & t0 <=' t by A1,Th86;
    take r,t0;
    thus thesis by A1,A3;
  end;
  suppose
A4: s <=' r;
    s = s+{} & {} <=' t by Th50,Th64;
    hence thesis by A2,A4;
  end;
end;

theorem
  for A being non empty Subset of RAT+ st A in RAT+ ex s st s in A & for
  r st r in A holds r <=' s
proof
  let A be non empty Subset of RAT+;
A1: now
    given i,j being Element of omega such that
A2: A = [i,j] and
A3: i,j are_relative_prime and
    j <> {} and
A4: j <> 1;
A5: now
      assume {i} in omega;
      then {} in {i} by ORDINAL3:8;
      then {} = i by TARSKI:def 1;
      hence contradiction by A3,A4,Th3;
    end;
    {i} in A by A2,TARSKI:def 2;
    then consider i1,j1 being Element of omega such that
A6: {i} = [i1,j1] and
A7: i1,j1 are_relative_prime and
    j1 <> {} and
A8: j1 <> 1 by A5,Th29;
    {i1,j1} in {i} by A6,TARSKI:def 2;
    then
A9: i = {i1,j1} by TARSKI:def 1;
    {i1} in {i} by A6,TARSKI:def 2;
    then i = {i1} by TARSKI:def 1;
    then j1 in {i1} by A9,TARSKI:def 2;
    then
A10: j1 = i1 by TARSKI:def 1;
    j1 = j1*^1 by ORDINAL2:39;
    hence contradiction by A7,A8,A10,Def2;
  end;
  assume A in RAT+;
  then reconsider B = A as Element of omega by A1,Th29;
A11: {} in B by ORDINAL3:8;
  now
    assume B is limit_ordinal;
    then omega c= B by A11,ORDINAL1:def 11;
    hence contradiction by ORDINAL1:5;
  end;
  then consider C such that
A12: B = succ C by ORDINAL1:29;
  C in B by A12,ORDINAL1:6;
  then reconsider C as ordinal Element of RAT+;
  take C;
  thus C in A by A12,ORDINAL1:6;
  let r;
  assume
A13: r in A;
  then r in B;
  then reconsider r as ordinal Element of RAT+;
  C-^r in omega by ORDINAL1:def 12;
  then reconsider x = C-^r as ordinal Element of RAT+ by Lm5;
  r c= C by A12,A13,ORDINAL1:22;
  then C = r+^x by ORDINAL3:def 5
    .= r+x by Th58;
  hence thesis by Def13;
end;

theorem
  ex t st r + t = s or s + t = r
proof
  r <=' s or s <=' r;
  hence thesis by Def13;
end;

theorem
  r < s implies ex t st r < t & t < s
proof
  assume
A1: r < s;
  then consider x such that
A2: s = r+x by Def13;
  consider y such that
A3: x = y+y by Th60;
  take t = r+y;
A4: s = t+y by A2,A3,Th51;
  then
A5: t <=' s by Def13;
  r <=' t by Def13;
  hence r < t by A1,A4,Th66;
  r <> s by A1;
  then s <> t by A4,Th62;
  hence thesis by A5,Th66;
end;

theorem
  ex s st r < s
proof
  take s = r+one;
  s+{} = s by Th50;
  then
A1: r <> s by Th62;
  r <=' s by Def13;
  hence thesis by A1,Th66;
end;

theorem
  t <> {} implies ex s st s in omega & r <=' s *' t
proof
  set y=((numerator r)*^(((numerator t)*^denominator r)-^1))/denominator r;
A1: denominator r <> {} by Th35;
  (denominator t)*^(numerator r) in omega by ORDINAL1:def 12;
  then reconsider
  s = (denominator t)*^(numerator r) as ordinal Element of RAT+ by Lm5;
  assume t <> {};
  then numerator t <> {} by Th37;
  then {} in (numerator t)*^denominator r by A1,ORDINAL3:8,31;
  then one c= (numerator t)*^denominator r by Lm3,ORDINAL1:21;
  then (numerator t)*^denominator r = 1+^(((numerator t)*^denominator r)-^ 1)
  by ORDINAL3:def 5;
  then
  s*^((numerator t)*^denominator r) = (denominator t)*^ ((numerator r)*^(1
  +^(((numerator t)*^denominator r)-^1))) by ORDINAL3:50
    .= (denominator t)*^((numerator r)*^1+^ (numerator r)*^(((numerator t)*^
  denominator r)-^1)) by ORDINAL3:46;
  then
A2: s*^(numerator t)*^denominator r = (denominator t)*^((numerator r)*^1+^
  (numerator r)*^(((numerator t)*^denominator r)-^1)) by ORDINAL3:50;
  take s;
  thus s in omega by ORDINAL1:def 12;
  take y;
  denominator t <> {} by Th35;
  then
  (s*^(numerator t))/denominator t = ((numerator r)*^1+^ (numerator r)*^(
  ((numerator t)*^denominator r)-^1))/denominator r by A1,A2,Th45
    .= (((numerator r)*^1)/denominator r)+y by Th35,Th47
    .= ((numerator r)/denominator r)+y by ORDINAL2:39
    .= r+y by Th39;
  then r+y = (s*^(numerator t))/(1*^denominator t) by ORDINAL2:39
    .= (s/1)*'((numerator t)/denominator t) by Th49
    .= s*'((numerator t)/denominator t) by Th40;
  hence thesis by Th39;
end;

scheme
  DisNat { n0,n1,n2() -> Element of RAT+, P[set] }: ex s st s in omega & P[s]
  & not P[s + n1()]
provided
A1: n1() = 1 and
A2: n0() = {} and
A3: n2() in omega and
A4: P[n0()] and
A5: not P[n2()]
proof
  defpred P1[Ordinal] means not P[$1] & $1 in omega;
A6: ex A st P1[A] by A3,A5;
  consider A such that
A7: P1[A] and
A8: for B st P1[B] holds A c= B from ORDINAL1:sch 1(A6);
A9: {} in A by A2,A4,A7,ORDINAL3:8;
  now
    assume A is limit_ordinal;
    then omega c= A by A9,ORDINAL1:def 11;
    then A in A by A7;
    hence contradiction;
  end;
  then consider B being Ordinal such that
A10: A = succ B by ORDINAL1:29;
A11: B in A by A10,ORDINAL1:8;
  then
A12: B in omega by A7,ORDINAL1:10;
  then reconsider s = B as ordinal Element of RAT+ by Lm5;
  take s;
  thus s in omega & P[s] by A8,A11,A12,ORDINAL1:5;
  A = B+^1 by A10,ORDINAL2:31;
  hence thesis by A1,A7,Th58;
end;