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₁[ 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₁[l] ;
ex k1 being Nat st
( S₁[k1] & ( for l1 being Nat st S₁[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