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 S1[ 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 S1[l] ;
ex k1 being Nat st
( S1[k1] & ( for l1 being Nat st S1[l1] holds
k1 <= l1 ) ) from 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