let p be Rational; :: thesis: ex m being Integer ex k being Nat st

( k <> 0 & p = m / k & ( for n being Integer

for w being Nat st w <> 0 & p = n / w holds

k <= w ) )

defpred S_{1}[ Nat] means ( $1 <> 0 & ex m1 being Integer st p = m1 / $1 );

ex m being Integer ex k being Nat st

( k <> 0 & p = m / k ) by Th5;

then A1: ex l being Nat st S_{1}[l]
;

ex k1 being Nat st

( S_{1}[k1] & ( for l1 being Nat st S_{1}[l1] holds

k1 <= l1 ) ) from NAT_1:sch 5(A1);

then consider k1 being Nat such that

A2: k1 <> 0 and

A3: ex m1 being Integer st p = m1 / k1 and

A4: for l1 being Nat st l1 <> 0 & ex n1 being Integer st p = n1 / l1 holds

k1 <= l1 ;

reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;

consider m1 being Integer such that

A5: p = m1 / k1 and

A6: for l1 being Nat st l1 <> 0 & ex n1 being Integer st p = n1 / l1 holds

k1 <= l1 by A3, A4;

take m1 ; :: thesis: ex k being Nat st

( k <> 0 & p = m1 / k & ( for n being Integer

for w being Nat st w <> 0 & p = n / w holds

k <= w ) )

take k1 ; :: thesis: ( k1 <> 0 & p = m1 / k1 & ( for n being Integer

for w being Nat st w <> 0 & p = n / w holds

k1 <= w ) )

thus k1 <> 0 by A2; :: thesis: ( p = m1 / k1 & ( for n being Integer

for w being Nat st w <> 0 & p = n / w holds

k1 <= w ) )

thus m1 / k1 = p by A5; :: thesis: for n being Integer

for w being Nat st w <> 0 & p = n / w holds

k1 <= w

thus for n being Integer

for w being Nat st w <> 0 & p = n / w holds

k1 <= w by A6; :: thesis: verum

( k <> 0 & p = m / k & ( for n being Integer

for w being Nat st w <> 0 & p = n / w holds

k <= w ) )

defpred S

ex m being Integer ex k being Nat st

( k <> 0 & p = m / k ) by Th5;

then A1: ex l being Nat st S

ex k1 being Nat st

( S

k1 <= l1 ) ) from NAT_1:sch 5(A1);

then consider k1 being Nat such that

A2: k1 <> 0 and

A3: ex m1 being Integer st p = m1 / k1 and

A4: for l1 being Nat st l1 <> 0 & ex n1 being Integer st p = n1 / l1 holds

k1 <= l1 ;

reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;

consider m1 being Integer such that

A5: p = m1 / k1 and

A6: for l1 being Nat st l1 <> 0 & ex n1 being Integer st p = n1 / l1 holds

k1 <= l1 by A3, A4;

take m1 ; :: thesis: ex k being Nat st

( k <> 0 & p = m1 / k & ( for n being Integer

for w being Nat st w <> 0 & p = n / w holds

k <= w ) )

take k1 ; :: thesis: ( k1 <> 0 & p = m1 / k1 & ( for n being Integer

for w being Nat st w <> 0 & p = n / w holds

k1 <= w ) )

thus k1 <> 0 by A2; :: thesis: ( p = m1 / k1 & ( for n being Integer

for w being Nat st w <> 0 & p = n / w holds

k1 <= w ) )

thus m1 / k1 = p by A5; :: thesis: for n being Integer

for w being Nat st w <> 0 & p = n / w holds

k1 <= w

thus for n being Integer

for w being Nat st w <> 0 & p = n / w holds

k1 <= w by A6; :: thesis: verum