consider m being Integer, k being Nat such that

A1: k <> 0 and

A2: p = m / k and

A3: for n being Integer

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

k <= w by Th6;

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

take IT = k; :: thesis: ( IT <> 0 & ex m being Integer st p = m / IT & ( for n being Integer

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

IT <= k ) )

thus ( IT <> 0 & ex m being Integer st p = m / IT & ( for n being Integer

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

IT <= k ) ) by A1, A2, A3; :: thesis: verum

A1: k <> 0 and

A2: p = m / k and

A3: for n being Integer

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

k <= w by Th6;

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

take IT = k; :: thesis: ( IT <> 0 & ex m being Integer st p = m / IT & ( for n being Integer

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

IT <= k ) )

thus ( IT <> 0 & ex m being Integer st p = m / IT & ( for n being Integer

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

IT <= k ) ) by A1, A2, A3; :: thesis: verum